Charlie is blue. Charlie is nice. Charlie is red. Charlie is round. Dave is big. Erin is big. Erin is cold. All cold, red things are blue. If Erin is blue then Erin is nice. If Erin is big then Erin is red. All blue things are nice. All big, nice things are red. All blue things are young. All big, cold things are red. All round things are big.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
All cold, red things are blue.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Erin is blue then Erin is nice.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "nice" "+"))
If Erin is big then Erin is red.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "red" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All big, nice things are red.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All big, cold things are red.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Erin is big.
True
1
proof
[(triple6)]
("Erin" "is" "big" "+")
triple6
Charlie is not red.
False
1
inv-proof
[(triple3 OR ((((triple4) -> rule8) triple2) -> rule5) OR ((((triple4) -> rule8) ((triple1) -> rule4)) -> rule5))]
("Charlie" "is" "red" "-")
triple3
((((triple4) -> (rule8 % int2)) triple2) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is big.
True
2
proof
[(((triple4) -> rule8))]
("Charlie" "is" "big" "+")
((triple4) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple4) -> rule8))]
("Charlie" "is" "big" "-")
((triple4) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is blue.
True
4
proof
[(((triple7 ((triple6) -> rule3)) -> rule1) OR ((triple7 ((triple6 triple7) -> rule7)) -> rule1))]
("Erin" "is" "blue" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple7 ((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((triple7 ((triple6) -> rule3)) -> rule1) OR ((triple7 ((triple6 triple7) -> rule7)) -> rule1))]
("Erin" "is" "blue" "-")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple7 ((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is young.
True
5
proof
[(((((triple7 ((triple6) -> rule3)) -> rule1)) -> rule6) OR ((((triple7 ((triple6 triple7) -> rule7)) -> rule1)) -> rule6))]
("Erin" "is" "young" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((((triple7 ((triple6) -> rule3)) -> rule1)) -> rule2) OR ((((triple7 ((triple6) -> rule3)) -> rule1)) -> rule4) OR ((((triple7 ((triple6 triple7) -> rule7)) -> rule1)) -> rule2) OR ((((triple7 ((triple6 triple7) -> rule7)) -> rule1)) -> rule4))]
("Erin" "is" "nice" "-")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "+")
Dave is not young.
Unknown
inv-rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is red.
Unknown
rconc
[@3: Dave is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is blue.[(triple1)] Charlie is nice.[(triple2 OR ((triple1) -> rule4))] Charlie is red.[(triple3 OR ((((triple4) -> rule8) triple2) -> rule5) OR ((((triple4) -> rule8) ((triple1) -> rule4)) -> rule5))] Charlie is round.[(triple4)] Dave is big.[(triple5)] Erin is big.[(triple6)] Erin is cold.[(triple7)] @1: Charlie is big.[(((triple4) -> rule8))] Charlie is young.[(((triple1) -> rule6))] Erin is red.[(((triple6) -> rule3) OR ((triple6 triple7) -> rule7))] @2: Erin is blue.[(((triple7 ((triple6) -> rule3)) -> rule1) OR ((triple7 ((triple6 triple7) -> rule7)) -> rule1))] @3: Erin is nice.[(((((triple7 ((triple6) -> rule3)) -> rule1)) -> rule2) OR ((((triple7 ((triple6) -> rule3)) -> rule1)) -> rule4) OR ((((triple7 ((triple6 triple7) -> rule7)) -> rule1)) -> rule2) OR ((((triple7 ((triple6 triple7) -> rule7)) -> rule1)) -> rule4))] Erin is young.[(((((triple7 ((triple6) -> rule3)) -> rule1)) -> rule6) OR ((((triple7 ((triple6 triple7) -> rule7)) -> rule1)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((((triple4) -> (rule8 % int2)) triple2) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
((triple4) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple6 triple7) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple7 ((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple7 ((triple6 triple7) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3