Bob is blue. Bob is young. Charlie is not blue. Charlie is red. Gary is quiet. Gary is round. Harry is red. If something is rough and red then it is not quiet. If Charlie is blue and Charlie is quiet then Charlie is round. All young things are round. If something is rough and not red then it is not big. Round things are not big. All round, red things are big.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is rough and red then it is not quiet.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "-"))
If Charlie is blue and Charlie is quiet then Charlie is round.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "round" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is rough and not red then it is not big.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "-"))
Round things are not big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "-"))
All round, red things are big.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Harry is red.
True
1
proof
[(triple7)]
("Harry" "is" "red" "+")
triple7
Charlie is blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "+")
triple3
Bob is round.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "round" "-")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is blue.[(triple1)] Bob is young.[(triple2)] Charlie is not blue.[(triple3)] Charlie is red.[(triple4)] Gary is quiet.[(triple5)] Gary is round.[(triple6)] Harry is red.[(triple7)] @1: Bob is round.[(((triple2) -> rule3))] Gary is not big.[(((triple6) -> rule5))] @2: Bob is not big.[(((((triple2) -> rule3)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is not big.
("Gary" "is" "big" "-")
((triple6) -> (rule5 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Bob is not big.
("Bob" "is" "big" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2