Bob is big. Bob is green. Charlie is nice. Erin is big. Erin is young. Gary is green. Gary is quiet. Round people are big. White, young people are green. All big people are quiet. Big people are white. If someone is quiet and green then they are nice. Quiet, big people are round. If Gary is round then Gary is young. If someone is quiet then they are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
White, young people are green.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet and green then they are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Quiet, big people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Gary is round then Gary is young.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "young" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Erin is young.
True
1
proof
[(triple5 OR ((((triple4) -> rule3)) -> rule8))]
("Erin" "is" "young" "+")
triple5
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Bob is not green.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule4) ((((triple1) -> rule3)) -> rule8)) -> rule2))]
("Bob" "is" "green" "-")
triple2
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple7) -> rule8))]
("Gary" "is" "young" "-")
((triple7) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Erin is green.
True
4
proof
[(((((triple4) -> rule4) triple5) -> rule2) OR ((((triple4) -> rule4) ((((triple4) -> rule3)) -> rule8)) -> rule2))]
("Erin" "is" "green" "+")
((((triple4) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Bob is not nice.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule5) OR ((((triple1) -> rule3) ((((triple1) -> rule4) ((((triple1) -> rule3)) -> rule8)) -> rule2)) -> rule5))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Erin is nice.
True
7
proof
[(((((triple4) -> rule3) ((((triple4) -> rule4) triple5) -> rule2)) -> rule5) OR ((((triple4) -> rule3) ((((triple4) -> rule4) ((((triple4) -> rule3)) -> rule8)) -> rule2)) -> rule5))]
("Erin" "is" "nice" "+")
((((triple4) -> (rule3 % int4)) ((((triple4) -> (rule4 % int3)) triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((triple4) -> (rule3 % int5)) ((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Erin is not nice.
False
7
inv-proof
[(((((triple4) -> rule3) ((((triple4) -> rule4) triple5) -> rule2)) -> rule5) OR ((((triple4) -> rule3) ((((triple4) -> rule4) ((((triple4) -> rule3)) -> rule8)) -> rule2)) -> rule5))]
("Erin" "is" "nice" "-")
((((triple4) -> (rule3 % int4)) ((((triple4) -> (rule4 % int3)) triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((triple4) -> (rule3 % int5)) ((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Gary is not white.
Unknown
inv-rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- FAIL)]]
("Gary" "is" "white" "-")
Charlie is young.
Unknown
rconc
[@4: Charlie is young.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule1 <- rule6 <- FAIL)]]
("Charlie" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2 OR ((((triple1) -> rule4) ((((triple1) -> rule3)) -> rule8)) -> rule2))] Charlie is nice.[(triple3)] Erin is big.[(triple4)] Erin is young.[(triple5 OR ((((triple4) -> rule3)) -> rule8))] Gary is green.[(triple6)] Gary is quiet.[(triple7)] @1: Bob is quiet.[(((triple1) -> rule3))] Bob is white.[(((triple1) -> rule4))] Erin is quiet.[(((triple4) -> rule3))] Erin is white.[(((triple4) -> rule4))] Gary is nice.[(((triple7 triple6) -> rule5))] Gary is young.[(((triple7) -> rule8))] @2: Bob is nice.[(((((triple1) -> rule3) triple2) -> rule5) OR ((((triple1) -> rule3) ((((triple1) -> rule4) ((((triple1) -> rule3)) -> rule8)) -> rule2)) -> rule5))] Bob is round.[(((((triple1) -> rule3) triple1) -> rule6))] Bob is young.[(((((triple1) -> rule3)) -> rule8))] Erin is green.[(((((triple4) -> rule4) triple5) -> rule2) OR ((((triple4) -> rule4) ((((triple4) -> rule3)) -> rule8)) -> rule2))] Erin is round.[(((((triple4) -> rule3) triple4) -> rule6))] @3: Erin is nice.[(((((triple4) -> rule3) ((((triple4) -> rule4) triple5) -> rule2)) -> rule5) OR ((((triple4) -> rule3) ((((triple4) -> rule4) ((((triple4) -> rule3)) -> rule8)) -> rule2)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7 triple6) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple7) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple4) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple4) -> (rule3 % int4)) ((((triple4) -> (rule4 % int3)) triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((triple4) -> (rule3 % int5)) ((((triple4) -> (rule4 % int4)) ((((triple4) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5