Anne is big. Anne is quiet. Anne is white. Bob is big. Bob is quiet. Charlie is quiet. Dave is white. If Dave is smart then Dave is green. White people are big. Green, big people are quiet. White people are smart. All white people are quiet. All furry, rough people are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
If Dave is smart then Dave is green.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Green, big people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All furry, rough people are white.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Bob is big.
True
1
proof
[(triple4)]
("Bob" "is" "big" "+")
triple4
Anne is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule2))]
("Anne" "is" "big" "-")
triple1
((triple3) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
True
2
proof
[(((triple3) -> rule4))]
("Anne" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple7) -> rule5) OR ((((((triple7) -> rule4)) -> rule1) ((triple7) -> rule2)) -> rule3))]
("Dave" "is" "quiet" "-")
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((((triple7) -> (rule4 % int4))) -> (rule1 % int3)) ((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is green.
True
3
proof
[(((((triple7) -> rule4)) -> rule1))]
("Dave" "is" "green" "+")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not green.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule1))]
("Dave" "is" "green" "-")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule2))] Anne is quiet.[(triple2 OR ((triple3) -> rule5))] Anne is white.[(triple3)] Bob is big.[(triple4)] Bob is quiet.[(triple5)] Charlie is quiet.[(triple6)] Dave is white.[(triple7)] @1: Anne is smart.[(((triple3) -> rule4))] Dave is big.[(((triple7) -> rule2))] Dave is quiet.[(((triple7) -> rule5) OR ((((((triple7) -> rule4)) -> rule1) ((triple7) -> rule2)) -> rule3))] Dave is smart.[(((triple7) -> rule4))] @2: Dave is green.[(((((triple7) -> rule4)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple7) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((((triple7) -> (rule4 % int4))) -> (rule1 % int3)) ((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Dave is smart.
("Dave" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2