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