Bob is nice. Fiona is green. Gary is big. Harry is cold. If Fiona is big and Fiona is cold then Fiona is young. If someone is nice and young then they are smart. All nice people are round. All green people are cold. Young, round people are green. Smart, round people are big. If Harry is nice then Harry is round. All round people are young.
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Fiona is big and Fiona is cold then Fiona is young.
((("Fiona" "is" "big" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "young" "+"))
If someone is nice and young then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Young, round people are green.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Smart, round people are big.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If Harry is nice then Harry is round.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "round" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Gary is big.
True
1
proof
[(triple3)]
("Gary" "is" "big" "+")
triple3
Fiona is not green.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "green" "-")
triple2
Fiona is cold.
True
2
proof
[(((triple2) -> rule4))]
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "round" "-")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Fiona is not young.
Unknown
inv-rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Gary is green.
Unknown
rconc
[@2: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Bob is nice.[(triple1)] Fiona is green.[(triple2)] Gary is big.[(triple3)] Harry is cold.[(triple4)] @1: Bob is round.[(((triple1) -> rule3))] Fiona is cold.[(((triple2) -> rule4))] @2: Bob is young.[(((((triple1) -> rule3)) -> rule8))] @3: Bob is green.[(((((((triple1) -> rule3)) -> rule8) ((triple1) -> rule3)) -> rule5))] Bob is smart.[(((triple1 ((((triple1) -> rule3)) -> rule8)) -> rule2))] @4: Bob is big.[(((((triple1 ((((triple1) -> rule3)) -> rule8)) -> rule2) ((triple1) -> rule3)) -> rule6))] Bob is cold.[(((((((((triple1) -> rule3)) -> rule8) ((triple1) -> rule3)) -> rule5)) -> rule4))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
((((triple1 ((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int4))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is cold.
("Bob" "is" "cold" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3)) ((triple1) -> (rule3 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4