Dave is cold. Dave is red. Dave is young. Gary is cold. Gary is round. Harry is cold. Harry is nice. Harry is red. Harry is white. Harry is young. If something is red then it is nice. If something is young and round then it is cold. All round, white things are cold. Round things are smart. All young things are round. If Harry is nice then Harry is smart. White, nice things are cold. Round, smart things are red.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is young and round then it is cold.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All round, white things are cold.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If Harry is nice then Harry is smart.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "smart" "+"))
White, nice things are cold.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Round, smart things are red.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Harry is cold.
True
1
proof
[(triple6 OR ((triple9 triple7) -> rule7) OR ((triple10 ((triple10) -> rule5)) -> rule2) OR ((triple9 ((triple8) -> rule1)) -> rule7) OR ((((triple10) -> rule5) triple9) -> rule3) OR ((triple9 ((((((triple10) -> rule5) ((((triple10) -> rule5)) -> rule4)) -> rule8)) -> rule1)) -> rule7))]
("Harry" "is" "cold" "+")
triple6
((triple9 triple7) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple10 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple10) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((((((triple10) -> (rule5 % int5)) ((((triple10) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5
Harry is not nice.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule1) OR ((((((triple10) -> rule5) ((((triple10) -> rule5)) -> rule4)) -> rule8)) -> rule1))]
("Harry" "is" "nice" "-")
triple7
((triple8) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((((triple10) -> (rule5 % int4)) ((((triple10) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Gary is smart.
True
2
proof
[(((triple5) -> rule4))]
("Gary" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple7) -> rule6) OR ((((triple10) -> rule5)) -> rule4) OR ((((triple8) -> rule1)) -> rule6))]
("Harry" "is" "smart" "-")
((triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is red.
True
4
proof
[(((triple5 ((triple5) -> rule4)) -> rule8))]
("Gary" "is" "red" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("Dave" "is" "smart" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is nice.
True
5
proof
[(((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule1))]
("Gary" "is" "nice" "+")
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not nice.
False
5
inv-proof
[(((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule1))]
("Gary" "is" "nice" "-")
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Dave is cold.[(triple1 OR ((triple3 ((triple3) -> rule5)) -> rule2))] Dave is red.[(triple2 OR ((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule4)) -> rule8))] Dave is young.[(triple3)] Gary is cold.[(triple4)] Gary is round.[(triple5)] Harry is cold.[(triple6 OR ((triple9 triple7) -> rule7) OR ((triple10 ((triple10) -> rule5)) -> rule2) OR ((triple9 ((triple8) -> rule1)) -> rule7) OR ((((triple10) -> rule5) triple9) -> rule3) OR ((triple9 ((((((triple10) -> rule5) ((((triple10) -> rule5)) -> rule4)) -> rule8)) -> rule1)) -> rule7))] Harry is nice.[(triple7 OR ((triple8) -> rule1) OR ((((((triple10) -> rule5) ((((triple10) -> rule5)) -> rule4)) -> rule8)) -> rule1))] Harry is red.[(triple8 OR ((((triple10) -> rule5) ((triple7) -> rule6)) -> rule8) OR ((((triple10) -> rule5) ((((triple10) -> rule5)) -> rule4)) -> rule8))] Harry is white.[(triple9)] Harry is young.[(triple10)] @1: Dave is nice.[(((triple2) -> rule1) OR ((((((triple3) -> rule5) ((((triple3) -> rule5)) -> rule4)) -> rule8)) -> rule1))] Dave is round.[(((triple3) -> rule5))] Gary is smart.[(((triple5) -> rule4))] Harry is round.[(((triple10) -> rule5))] Harry is smart.[(((triple7) -> rule6) OR ((((triple10) -> rule5)) -> rule4) OR ((((triple8) -> rule1)) -> rule6))] @2: Dave is smart.[(((((triple3) -> rule5)) -> rule4))] Gary is red.[(((triple5 ((triple5) -> rule4)) -> rule8))] @3: Gary is nice.[(((((triple5 ((triple5) -> rule4)) -> rule8)) -> rule1))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
((triple3 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple2
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((triple9 triple7) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple10 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((triple8) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple10) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((((((triple10) -> (rule5 % int5)) ((((triple10) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
int5
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((triple8) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((((triple10) -> (rule5 % int4)) ((((triple10) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple8
((((triple10) -> (rule5 % int3)) ((triple7) -> (rule6 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((triple10) -> (rule5 % int3)) ((((triple10) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((((triple3) -> (rule5 % int4)) ((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple10) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple5 ((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3