Anne is not red. Charlie is rough. Dave is nice. Dave is red. Dave is round. Harry is big. Harry is nice. If Charlie is round then Charlie is not rough. If something is red then it is nice. If something is nice then it is not cold. All rough things are red. If Anne is cold and Anne is red then Anne is big. If something is nice and big then it is not furry. If something is rough and not cold then it is big. Cold things are big. If something is nice and not round then it is big.
Anne is not red.
("Anne" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Charlie is round then Charlie is not rough.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "rough" "-"))
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is not cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Anne is cold and Anne is red then Anne is big.
((("Anne" "is" "cold" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "big" "+"))
If something is nice and big then it is not furry.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "-"))
If something is rough and not cold then it is big.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "is" "big" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is nice and not round then it is big.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
Anne is not red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Anne is red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not cold.
True
2
proof
[(((triple7) -> rule3))]
("Harry" "is" "cold" "-")
((triple7) -> (rule3 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is cold.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "cold" "+")
((triple7) -> (rule3 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Charlie is nice.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not cold.
True
4
proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule3))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is cold.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule3))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
True
6
proof
[(((triple2 ((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule7))]
("Charlie" "is" "big" "+")
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is not big.
False
6
inv-proof
[(((triple2 ((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule7))]
("Charlie" "is" "big" "-")
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is not furry.
True
10
proof
[(((((((triple2) -> rule4)) -> rule2) ((triple2 ((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule7)) -> rule6))]
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule4 % int5))) -> (rule2 % int4)) ((triple2 ((((((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
Charlie is furry.
False
10
inv-proof
[(((((((triple2) -> rule4)) -> rule2) ((triple2 ((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule7)) -> rule6))]
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule4 % int5))) -> (rule2 % int4)) ((triple2 ((((((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "big" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "red" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is not red.[(triple1)] Charlie is rough.[(triple2)] Dave is nice.[(triple3 OR ((triple4) -> rule2))] Dave is red.[(triple4)] Dave is round.[(triple5)] Harry is big.[(triple6)] Harry is nice.[(triple7)] @1: Charlie is red.[(((triple2) -> rule4))] Dave is not cold.[(((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))] Harry is not cold.[(((triple7) -> rule3))] Harry is not furry.[(((triple7 triple6) -> rule6))] @2: Charlie is nice.[(((((triple2) -> rule4)) -> rule2))] @3: Charlie is not cold.[(((((((triple2) -> rule4)) -> rule2)) -> rule3))] @4: Charlie is big.[(((triple2 ((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule7))] @5: Charlie is not furry.[(((((((triple2) -> rule4)) -> rule2) ((triple2 ((((((triple2) -> rule4)) -> rule2)) -> rule3)) -> rule7)) -> rule6))]
Anne is not red.
("Anne" "is" "red" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple4) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
((triple2) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
((triple3) -> (rule3 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is not cold.
("Harry" "is" "cold" "-")
((triple7) -> (rule3 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is not furry.
("Harry" "is" "furry" "-")
((triple7 triple6) -> (rule6 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule4 % int5))) -> (rule2 % int4)) ((triple2 ((((((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5