Bob is round. Charlie is red. Erin is young. Harry is green. If someone is round and cold then they are blue. If Harry is green then Harry is young. All kind people are young. Green people are blue. If Harry is blue then Harry is cold. All round, young people are cold. If Bob is young and Bob is green then Bob is red. If Charlie is kind then Charlie is cold.
Bob is round.
("Bob" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is round and cold then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Harry is green then Harry is young.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "young" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Harry is blue then Harry is cold.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "cold" "+"))
All round, young people are cold.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Bob is young and Bob is green then Bob is red.
((("Bob" "is" "young" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "red" "+"))
If Charlie is kind then Charlie is cold.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "cold" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Bob is not blue.
Unknown
inv-rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Bob is round.[(triple1)] Charlie is red.[(triple2)] Erin is young.[(triple3)] Harry is green.[(triple4)] @1: Harry is blue.[(((triple4) -> rule4))] Harry is young.[(((triple4) -> rule2))] @2: Harry is cold.[(((((triple4) -> rule4)) -> rule5))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2