Dave is big. Dave is cold. Dave is red. Dave is round. Dave is young. Harry is cold. Harry is young. Young things are round. If something is kind and not rough then it is not young. Rough things are young. Big things are kind. If something is young and not red then it is not big. If something is round and big then it is cold. If Harry is young and Harry is round then Harry is big. If Harry is kind then Harry is round.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is young.
("Harry" "is" "young" "+")
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is kind and not rough then it is not young.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "young" "-"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is young and not red then it is not big.
((("something" "is" "young" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "-"))
If something is round and big then it is cold.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Harry is young and Harry is round then Harry is big.
((("Harry" "is" "young" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "big" "+"))
If Harry is kind then Harry is round.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
Harry is cold.
True
1
proof
[(triple6 OR ((((triple7) -> rule1) ((triple7 ((triple7) -> rule1)) -> rule7)) -> rule6))]
("Harry" "is" "cold" "+")
triple6
((((triple7) -> (rule1 % int3)) ((triple7 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Harry is round.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is big.
True
4
proof
[(((triple7 ((triple7) -> rule1)) -> rule7))]
("Harry" "is" "big" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not big.
False
4
inv-proof
[(((triple7 ((triple7) -> rule1)) -> rule7))]
("Harry" "is" "big" "-")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
True
5
proof
[(((((triple7 ((triple7) -> rule1)) -> rule7)) -> rule4))]
("Harry" "is" "kind" "+")
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not kind.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule1)) -> rule7)) -> rule4))]
("Harry" "is" "kind" "-")
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2 OR ((triple4 triple1) -> rule6) OR ((((triple5) -> rule1) triple1) -> rule6))] Dave is red.[(triple3)] Dave is round.[(triple4 OR ((triple5) -> rule1))] Dave is young.[(triple5)] Harry is cold.[(triple6 OR ((((triple7) -> rule1) ((triple7 ((triple7) -> rule1)) -> rule7)) -> rule6))] Harry is young.[(triple7)] @1: Dave is kind.[(((triple1) -> rule4))] Harry is round.[(((triple7) -> rule1))] @2: Harry is big.[(((triple7 ((triple7) -> rule1)) -> rule7))] @3: Harry is kind.[(((((triple7 ((triple7) -> rule1)) -> rule7)) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple5) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((((triple7) -> (rule1 % int3)) ((triple7 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3