Anne is nice. Anne is smart. Charlie is big. Charlie is cold. Charlie is nice. Charlie is round. Charlie is smart. Harry is big. Harry is cold. Harry is kind. Harry is smart. Harry is young. If Charlie is young and Charlie is nice then Charlie is smart. Big, smart things are cold. Smart things are round. All kind things are nice. If something is young then it is smart. All round things are big.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Charlie is young and Charlie is nice then Charlie is smart.
((("Charlie" "is" "young" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "smart" "+"))
Big, smart things are cold.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Charlie is not big.
False
1
inv-proof
[(triple3 OR ((triple6) -> rule6) OR ((((triple7) -> rule3)) -> rule6))]
("Charlie" "is" "big" "-")
triple3
((triple6) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Anne is round.
True
2
proof
[(((triple2) -> rule3))]
("Anne" "is" "round" "+")
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple10) -> rule4))]
("Harry" "is" "nice" "-")
((triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Anne is big.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("Anne" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("Anne" "is" "big" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
True
5
proof
[(((((((triple2) -> rule3)) -> rule6) triple2) -> rule2))]
("Anne" "is" "cold" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((((((triple2) -> rule3)) -> rule6) triple2) -> rule2))]
("Anne" "is" "cold" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is nice.[(triple1)] Anne is smart.[(triple2)] Charlie is big.[(triple3 OR ((triple6) -> rule6) OR ((((triple7) -> rule3)) -> rule6))] Charlie is cold.[(triple4 OR ((triple3 triple7) -> rule2) OR ((((triple6) -> rule6) triple7) -> rule2) OR ((((((triple7) -> rule3)) -> rule6) triple7) -> rule2))] Charlie is nice.[(triple5)] Charlie is round.[(triple6 OR ((triple7) -> rule3))] Charlie is smart.[(triple7)] Harry is big.[(triple8 OR ((((triple11) -> rule3)) -> rule6) OR ((((((triple12) -> rule5)) -> rule3)) -> rule6))] Harry is cold.[(triple9 OR ((triple8 triple11) -> rule2) OR ((triple8 ((triple12) -> rule5)) -> rule2) OR ((((((triple11) -> rule3)) -> rule6) triple11) -> rule2) OR ((((((triple11) -> rule3)) -> rule6) ((triple12) -> rule5)) -> rule2) OR ((((((((triple12) -> rule5)) -> rule3)) -> rule6) triple11) -> rule2) OR ((((((((triple12) -> rule5)) -> rule3)) -> rule6) ((triple12) -> rule5)) -> rule2))] Harry is kind.[(triple10)] Harry is smart.[(triple11 OR ((triple12) -> rule5))] Harry is young.[(triple12)] @1: Anne is round.[(((triple2) -> rule3))] Harry is nice.[(((triple10) -> rule4))] Harry is round.[(((triple11) -> rule3) OR ((((triple12) -> rule5)) -> rule3))] @2: Anne is big.[(((((triple2) -> rule3)) -> rule6))] @3: Anne is cold.[(((((((triple2) -> rule3)) -> rule6) triple2) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
((triple6) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((triple3 triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple7) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
((((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((((triple12) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple8 triple11) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple8 ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple11) -> (rule3 % int3))) -> (rule6 % int2)) triple11) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((((triple11) -> (rule3 % int4))) -> (rule6 % int3)) ((triple12) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((((((triple12) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) triple11) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((((triple12) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) ((triple12) -> (rule5 % int4))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple12) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple10) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple11) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple12) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3