Charlie is big. Charlie is quiet. Charlie is young. Harry is kind. Harry is nice. Harry is quiet. Harry is young. Big, cold people are kind. All young, quiet people are cold. If Charlie is big and Charlie is kind then Charlie is nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Big, cold people are kind.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All young, quiet people are cold.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is big and Charlie is kind then Charlie is nice.
((("Charlie" "is" "big" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "nice" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Harry is cold.
True
3
proof
[(((triple7 triple6) -> rule2))]
("Harry" "is" "cold" "+")
((triple7 triple6) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is not cold.
False
3
inv-proof
[(((triple3 triple2) -> rule2))]
("Charlie" "is" "cold" "-")
((triple3 triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
True
5
proof
[(((triple1 ((triple3 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "kind" "+")
((triple1 ((triple3 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not kind.
False
5
inv-proof
[(((triple1 ((triple3 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "kind" "-")
((triple1 ((triple3 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
True
7
proof
[(((triple1 ((triple1 ((triple3 triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "+")
((triple1 ((triple1 ((triple3 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is not nice.
False
7
inv-proof
[(((triple1 ((triple1 ((triple3 triple2) -> rule2)) -> rule1)) -> rule3))]
("Charlie" "is" "nice" "-")
((triple1 ((triple1 ((triple3 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is quiet.[(triple2)] Charlie is young.[(triple3)] Harry is kind.[(triple4)] Harry is nice.[(triple5)] Harry is quiet.[(triple6)] Harry is young.[(triple7)] @1: Charlie is cold.[(((triple3 triple2) -> rule2))] Harry is cold.[(((triple7 triple6) -> rule2))] @2: Charlie is kind.[(((triple1 ((triple3 triple2) -> rule2)) -> rule1))] @3: Charlie is nice.[(((triple1 ((triple1 ((triple3 triple2) -> rule2)) -> rule1)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3 triple2) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple7 triple6) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 ((triple3 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1 ((triple1 ((triple3 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3