Bob is big. Bob is blue. Bob is red. Bob is young. Charlie is white. Erin is blue. Erin is white. Gary is nice. Gary is not red. Gary is not white. Gary is not young. All young things are blue. Young, round things are red. If something is big and blue then it is young. If something is red then it is young. All red things are nice. White things are round. If something is round then it is big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is not white.
("Gary" "is" "white" "-")
Gary is not young.
("Gary" "is" "young" "-")
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Young, round things are red.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is big and blue then it is young.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Gary is not red.
True
1
proof
[(triple9)]
("Gary" "is" "red" "-")
triple9
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Erin is round.
True
2
proof
[(((triple7) -> rule6))]
("Erin" "is" "round" "+")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple7) -> rule6))]
("Erin" "is" "round" "-")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is big.
True
3
proof
[(((((triple5) -> rule6)) -> rule7))]
("Charlie" "is" "big" "+")
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule7))]
("Erin" "is" "big" "-")
((((triple7) -> (rule6 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
True
5
proof
[(((((((triple7) -> rule6)) -> rule7) triple6) -> rule3))]
("Erin" "is" "young" "+")
((((((triple7) -> (rule6 % int3))) -> (rule7 % int2)) triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not young.
False
5
inv-proof
[(((((((triple7) -> rule6)) -> rule7) triple6) -> rule3))]
("Erin" "is" "young" "-")
((((((triple7) -> (rule6 % int3))) -> (rule7 % int2)) triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
True
8
proof
[(((((((((triple7) -> rule6)) -> rule7) triple6) -> rule3) ((triple7) -> rule6)) -> rule2))]
("Erin" "is" "red" "+")
((((((((triple7) -> (rule6 % int4))) -> (rule7 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule6 % int4))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is not red.
False
8
inv-proof
[(((((((((triple7) -> rule6)) -> rule7) triple6) -> rule3) ((triple7) -> rule6)) -> rule2))]
("Erin" "is" "red" "-")
((((((((triple7) -> (rule6 % int4))) -> (rule7 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule6 % int4))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is nice.
True
9
proof
[(((((((((((triple7) -> rule6)) -> rule7) triple6) -> rule3) ((triple7) -> rule6)) -> rule2)) -> rule5))]
("Erin" "is" "nice" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule7 % int4)) triple6) -> (rule3 % int3)) ((triple7) -> (rule6 % int5))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Erin is not nice.
False
9
inv-proof
[(((((((((((triple7) -> rule6)) -> rule7) triple6) -> rule3) ((triple7) -> rule6)) -> rule2)) -> rule5))]
("Erin" "is" "nice" "-")
((((((((((triple7) -> (rule6 % int5))) -> (rule7 % int4)) triple6) -> (rule3 % int3)) ((triple7) -> (rule6 % int5))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is blue.
Unknown
rconc
[@4: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Charlie is young.
Unknown
rconc
[@4: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "young" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Gary is big.
Unknown
rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple4) -> rule1) OR ((((triple3) -> rule4)) -> rule1))] Bob is red.[(triple3)] Bob is young.[(triple4 OR ((triple3) -> rule4) OR ((triple1 triple2) -> rule3))] Charlie is white.[(triple5)] Erin is blue.[(triple6)] Erin is white.[(triple7)] Gary is nice.[(triple8)] Gary is not red.[(triple9)] Gary is not white.[(triple10)] Gary is not young.[(triple11)] @1: Bob is nice.[(((triple3) -> rule5))] Charlie is round.[(((triple5) -> rule6))] Erin is round.[(((triple7) -> rule6))] @2: Charlie is big.[(((((triple5) -> rule6)) -> rule7))] Erin is big.[(((((triple7) -> rule6)) -> rule7))] @3: Erin is young.[(((((((triple7) -> rule6)) -> rule7) triple6) -> rule3))] @4: Erin is red.[(((((((((triple7) -> rule6)) -> rule7) triple6) -> rule3) ((triple7) -> rule6)) -> rule2))] @5: Erin is nice.[(((((((((((triple7) -> rule6)) -> rule7) triple6) -> rule3) ((triple7) -> rule6)) -> rule2)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple3) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is not red.
("Gary" "is" "red" "-")
triple9
Gary is not white.
("Gary" "is" "white" "-")
triple10
Gary is not young.
("Gary" "is" "young" "-")
triple11
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple5) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((triple7) -> (rule6 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((((triple7) -> (rule6 % int3))) -> (rule7 % int2)) triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((((((triple7) -> (rule6 % int4))) -> (rule7 % int3)) triple6) -> (rule3 % int2)) ((triple7) -> (rule6 % int4))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
((((((((((triple7) -> (rule6 % int5))) -> (rule7 % int4)) triple6) -> (rule3 % int3)) ((triple7) -> (rule6 % int5))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
int5