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