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