Bob is big. Dave is green. Dave is nice. Dave is round. Erin is cold. Erin is red. Harry is cold. Harry is quiet. Harry is red. Harry is round. Red things are big. Cold, green things are nice. All round, nice things are green. If something is nice then it is round. If something is quiet then it is red. Round, cold things are big. Green things are cold. If something is cold then it is nice.
Bob is big.
("Bob" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Cold, green things are nice.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All round, nice things are green.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Round, cold things are big.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Harry is round.
True
1
proof
[(triple10 OR ((((triple7) -> rule8)) -> rule4))]
("Harry" "is" "round" "+")
triple10
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Erin is not red.
False
1
inv-proof
[(triple6)]
("Erin" "is" "red" "-")
triple6
Erin is nice.
True
2
proof
[(((triple5) -> rule8))]
("Erin" "is" "nice" "+")
((triple5) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple2) -> rule7) OR ((((triple4 triple3) -> rule3)) -> rule7) OR ((((((triple3) -> rule4) triple3) -> rule3)) -> rule7))]
("Dave" "is" "cold" "-")
((triple2) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4 triple3) -> (rule3 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@4: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule3 <- rule8 <- FAIL)]]
("Bob" "is" "nice" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "red" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Dave is green.[(triple2 OR ((triple4 triple3) -> rule3) OR ((((triple3) -> rule4) triple3) -> rule3))] Dave is nice.[(triple3 OR ((((triple2) -> rule7)) -> rule8) OR ((((triple2) -> rule7) triple2) -> rule2))] Dave is round.[(triple4 OR ((triple3) -> rule4) OR ((((((triple2) -> rule7)) -> rule8)) -> rule4) OR ((((((triple2) -> rule7) triple2) -> rule2)) -> rule4))] Erin is cold.[(triple5)] Erin is red.[(triple6)] Harry is cold.[(triple7)] Harry is quiet.[(triple8)] Harry is red.[(triple9 OR ((triple8) -> rule5))] Harry is round.[(triple10 OR ((((triple7) -> rule8)) -> rule4))] @1: Dave is cold.[(((triple2) -> rule7) OR ((((triple4 triple3) -> rule3)) -> rule7) OR ((((((triple3) -> rule4) triple3) -> rule3)) -> rule7))] Erin is big.[(((triple6) -> rule1) OR ((((((triple5) -> rule8)) -> rule4) triple5) -> rule6))] Erin is nice.[(((triple5) -> rule8))] Harry is big.[(((triple9) -> rule1) OR ((triple10 triple7) -> rule6) OR ((((triple8) -> rule5)) -> rule1) OR ((((((triple7) -> rule8)) -> rule4) triple7) -> rule6))] Harry is nice.[(((triple7) -> rule8))] @2: Dave is big.[(((triple4 ((triple2) -> rule7)) -> rule6) OR ((((triple3) -> rule4) ((triple2) -> rule7)) -> rule6) OR ((triple4 ((((triple4 triple3) -> rule3)) -> rule7)) -> rule6) OR ((((triple3) -> rule4) ((((triple4 triple3) -> rule3)) -> rule7)) -> rule6) OR ((triple4 ((((((triple3) -> rule4) triple3) -> rule3)) -> rule7)) -> rule6) OR ((((triple3) -> rule4) ((((((triple3) -> rule4) triple3) -> rule3)) -> rule7)) -> rule6) OR ((((((((triple2) -> rule7)) -> rule8)) -> rule4) ((triple2) -> rule7)) -> rule6) OR ((((((((triple2) -> rule7) triple2) -> rule2)) -> rule4) ((triple2) -> rule7)) -> rule6) OR ((((((((triple2) -> rule7)) -> rule8)) -> rule4) ((((triple4 triple3) -> rule3)) -> rule7)) -> rule6) OR ((((((((triple2) -> rule7) triple2) -> rule2)) -> rule4) ((((triple4 triple3) -> rule3)) -> rule7)) -> rule6) OR ((((((((triple2) -> rule7)) -> rule8)) -> rule4) ((((((triple3) -> rule4) triple3) -> rule3)) -> rule7)) -> rule6) OR ((((((((triple2) -> rule7) triple2) -> rule2)) -> rule4) ((((((triple3) -> rule4) triple3) -> rule3)) -> rule7)) -> rule6))] Erin is round.[(((((triple5) -> rule8)) -> rule4))] Harry is green.[(((triple10 ((triple7) -> rule8)) -> rule3) OR ((((((triple7) -> rule8)) -> rule4) ((triple7) -> rule8)) -> rule3))] @3: Erin is green.[(((((((triple5) -> rule8)) -> rule4) ((triple5) -> rule8)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple4 triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple3) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
((((((triple2) -> (rule7 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
((triple8) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple10
((((triple7) -> (rule8 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4 triple3) -> (rule3 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple5) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple10 triple7) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple4 ((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple4 ((((triple4 triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple3) -> (rule4 % int4)) ((((triple4 triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((triple4 ((((((triple3) -> (rule4 % int4)) triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple3) -> (rule4 % int4)) ((((((triple3) -> (rule4 % int4)) triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((((((triple2) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule7 % int4))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((((triple2) -> (rule7 % int4)) triple2) -> (rule2 % int3))) -> (rule4 % int2)) ((triple2) -> (rule7 % int4))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
((((((((triple2) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule4 % int3)) ((((triple4 triple3) -> (rule3 % int2))) -> (rule7 % int5))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
((((((((triple2) -> (rule7 % int5)) triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple4 triple3) -> (rule3 % int2))) -> (rule7 % int5))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
((((((((triple2) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule4 % int3)) ((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int5))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
((((((((triple2) -> (rule7 % int5)) triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((((triple3) -> (rule4 % int3)) triple3) -> (rule3 % int2))) -> (rule7 % int5))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
Erin is round.
("Erin" "is" "round" "+")
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple10 ((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple7) -> (rule8 % int3))) -> (rule4 % int2)) ((triple7) -> (rule8 % int3))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple5) -> (rule8 % int3))) -> (rule4 % int2)) ((triple5) -> (rule8 % int3))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3