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