Dave is cold. Harry is quiet. Harry is young. If Dave is cold then Dave is nice. All kind things are big. All young things are cold. If something is kind then it is nice. All nice, big things are kind. All cold, young things are kind. All smart, big things are young. If Dave is nice and Dave is cold then Dave is young.
Dave is cold.
("Dave" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is cold then Dave is nice.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All nice, big things are kind.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
All cold, young things are kind.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All smart, big things are young.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Dave is nice and Dave is cold then Dave is young.
((("Dave" "is" "nice" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "young" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Harry is cold.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "cold" "-")
((triple3) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is cold.[(triple1)] Harry is quiet.[(triple2)] Harry is young.[(triple3)] @1: Dave is nice.[(((triple1) -> rule1))] Harry is cold.[(((triple3) -> rule3))] @2: Dave is young.[(((((triple1) -> rule1) triple1) -> rule8))] Harry is kind.[(((((triple3) -> rule3) triple3) -> rule6))] @3: Dave is kind.[(((triple1 ((((triple1) -> rule1) triple1) -> rule8)) -> rule6))] Harry is big.[(((((((triple3) -> rule3) triple3) -> rule6)) -> rule2))] Harry is nice.[(((((((triple3) -> rule3) triple3) -> rule6)) -> rule4))] @4: Dave is big.[(((((triple1 ((((triple1) -> rule1) triple1) -> rule8)) -> rule6)) -> rule2))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule8 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule6 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((triple1 ((((triple1) -> (rule1 % int4)) triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4