Charlie is big. Charlie is round. Charlie is young. All big, quiet things are round. All big things are white. If something is big then it is cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All big, quiet things are round.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Charlie is round.
True
1
proof
[(triple2)]
("Charlie" "is" "round" "+")
triple2
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is white.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "white" "+")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "white" "-")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Charlie is round.[(triple2)] Charlie is young.[(triple3)] @1: Charlie is cold.[(((triple1) -> rule3))] Charlie is white.[(((triple1) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1