Bob is big. Bob is red. Charlie is green. Charlie is kind. Charlie is red. Charlie is round. Charlie is smart. Charlie is white. Dave is big. Dave is red. Dave is round. Dave is smart. Smart, big people are green. If someone is green and kind then they are big. If someone is white then they are green. All big, kind people are red. If someone is green then they are round. If someone is round and smart then they are green.
Bob is big.
("Bob" "is" "big" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Smart, big people are green.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is green and kind then they are big.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All big, kind people are red.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is round and smart then they are green.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Dave is smart.
True
1
proof
[(triple12)]
("Dave" "is" "smart" "+")
triple12
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Charlie is big.
True
3
proof
[(((triple3 triple4) -> rule2) OR ((((triple8) -> rule3) triple4) -> rule2) OR ((((triple6 triple7) -> rule6) triple4) -> rule2))]
("Charlie" "is" "big" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple8) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6 triple7) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((triple3 triple4) -> rule2) OR ((((triple8) -> rule3) triple4) -> rule2) OR ((((triple6 triple7) -> rule6) triple4) -> rule2))]
("Charlie" "is" "big" "-")
((triple3 triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple8) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6 triple7) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is red.[(triple2)] Charlie is green.[(triple3 OR ((triple8) -> rule3) OR ((triple6 triple7) -> rule6))] Charlie is kind.[(triple4)] Charlie is red.[(triple5 OR ((((triple3 triple4) -> rule2) triple4) -> rule4) OR ((((((triple8) -> rule3) triple4) -> rule2) triple4) -> rule4) OR ((((((triple6 triple7) -> rule6) triple4) -> rule2) triple4) -> rule4))] Charlie is round.[(triple6 OR ((triple3) -> rule5) OR ((((triple8) -> rule3)) -> rule5))] Charlie is smart.[(triple7)] Charlie is white.[(triple8)] Dave is big.[(triple9)] Dave is red.[(triple10)] Dave is round.[(triple11 OR ((((triple12 triple9) -> rule1)) -> rule5))] Dave is smart.[(triple12)] @1: Charlie is big.[(((triple3 triple4) -> rule2) OR ((((triple8) -> rule3) triple4) -> rule2) OR ((((triple6 triple7) -> rule6) triple4) -> rule2))] Dave is green.[(((triple11 triple12) -> rule6) OR ((triple12 triple9) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple8) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple6 triple7) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((((triple3 triple4) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple8) -> (rule3 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((((triple6 triple7) -> (rule6 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple3) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is round.
("Dave" "is" "round" "+")
triple11
((((triple12 triple9) -> (rule1 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple8) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((triple6 triple7) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple11 triple12) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple12 triple9) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1