Bob is cold. Bob is quiet. Bob is rough. Bob is young. Charlie is not round. Charlie is white. Charlie is not young. If someone is big and rough then they are not cold. If someone is rough then they are not round. If someone is quiet and not young then they are not round. If someone is big and quiet then they are round. If Charlie is big then Charlie is rough. White, round people are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
If someone is big and rough then they are not cold.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "-"))
If someone is rough then they are not round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "-"))
If someone is quiet and not young then they are not round.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "-"))
If someone is big and quiet then they are round.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Charlie is big then Charlie is rough.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "rough" "+"))
White, round people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is white.
True
1
proof
[(triple6)]
("Charlie" "is" "white" "+")
triple6
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Bob is not round.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is round.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "round" "+")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is quiet.[(triple2)] Bob is rough.[(triple3)] Bob is young.[(triple4)] Charlie is not round.[(triple5)] Charlie is not young.[(triple7)] Charlie is white.[(triple6)] @1: Bob is not round.[(((triple3) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is not round.
("Charlie" "is" "round" "-")
triple5
Charlie is not young.
("Charlie" "is" "young" "-")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Bob is not round.
("Bob" "is" "round" "-")
((triple3) -> (rule2 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1