Bob is round. Charlie is blue. Charlie is young. If Bob is round then Bob is red. If Bob is red then Bob is young.
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Bob is round then Bob is red.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "red" "+"))
If Bob is red then Bob is young.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "young" "+"))
Charlie is young.
True
1
proof
[(triple3)]
("Charlie" "is" "young" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "young" "-")
triple3
Bob is red.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "red" "-")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "young" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is round.[(triple1)] Charlie is blue.[(triple2)] Charlie is young.[(triple3)] @1: Bob is red.[(((triple1) -> rule1))] @2: Bob is young.[(((((triple1) -> rule1)) -> rule2))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2