Dave is smart. Dave is young. Erin is smart. Gary is blue. Gary is young. Harry is cold. Harry is smart. Nice, smart people are blue. If someone is smart then they are young. If someone is quiet and smart then they are young. If someone is smart and young then they are nice. Cold people are big. If someone is quiet then they are cold. Blue people are cold.
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Nice, smart people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet and smart then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If someone is smart and young then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Dave is young.
True
1
proof
[(triple2 OR ((triple1) -> rule2))]
("Dave" "is" "young" "+")
triple2
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple1)]
("Dave" "is" "smart" "-")
triple1
Erin is young.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "young" "+")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple4) -> rule7))]
("Gary" "is" "cold" "-")
((triple4) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Dave is blue.
True
5
proof
[(((((triple1 triple2) -> rule4) triple1) -> rule1) OR ((((triple1 ((triple1) -> rule2)) -> rule4) triple1) -> rule1))]
("Dave" "is" "blue" "+")
((((triple1 triple2) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((((triple1 triple2) -> rule4) triple1) -> rule1) OR ((((triple1 ((triple1) -> rule2)) -> rule4) triple1) -> rule1))]
("Dave" "is" "blue" "-")
((((triple1 triple2) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Harry is blue.
True
6
proof
[(((((triple7 ((triple7) -> rule2)) -> rule4) triple7) -> rule1))]
("Harry" "is" "blue" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not blue.
False
6
inv-proof
[(((((triple7 ((triple7) -> rule2)) -> rule4) triple7) -> rule1))]
("Harry" "is" "blue" "-")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Erin is cold.
True
7
proof
[(((((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1)) -> rule7))]
("Erin" "is" "cold" "+")
((((((triple3 ((triple3) -> (rule2 % int4))) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is not cold.
False
7
inv-proof
[(((((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1)) -> rule7))]
("Erin" "is" "cold" "-")
((((((triple3 ((triple3) -> (rule2 % int4))) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is big.
True
8
proof
[(((((((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1)) -> rule7)) -> rule5))]
("Erin" "is" "big" "+")
((((((((triple3 ((triple3) -> (rule2 % int5))) -> (rule4 % int4)) triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Erin is not big.
False
8
inv-proof
[(((((((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1)) -> rule7)) -> rule5))]
("Erin" "is" "big" "-")
((((((((triple3 ((triple3) -> (rule2 % int5))) -> (rule4 % int4)) triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Dave is smart.[(triple1)] Dave is young.[(triple2 OR ((triple1) -> rule2))] Erin is smart.[(triple3)] Gary is blue.[(triple4)] Gary is young.[(triple5)] Harry is cold.[(triple6 OR ((((((triple7 ((triple7) -> rule2)) -> rule4) triple7) -> rule1)) -> rule7))] Harry is smart.[(triple7)] @1: Dave is nice.[(((triple1 triple2) -> rule4) OR ((triple1 ((triple1) -> rule2)) -> rule4))] Erin is young.[(((triple3) -> rule2))] Gary is cold.[(((triple4) -> rule7))] Harry is big.[(((triple6) -> rule5) OR ((((((((triple7 ((triple7) -> rule2)) -> rule4) triple7) -> rule1)) -> rule7)) -> rule5))] Harry is young.[(((triple7) -> rule2))] @2: Dave is blue.[(((((triple1 triple2) -> rule4) triple1) -> rule1) OR ((((triple1 ((triple1) -> rule2)) -> rule4) triple1) -> rule1))] Erin is nice.[(((triple3 ((triple3) -> rule2)) -> rule4))] Gary is big.[(((((triple4) -> rule7)) -> rule5))] Harry is nice.[(((triple7 ((triple7) -> rule2)) -> rule4))] @3: Dave is cold.[(((((((triple1 triple2) -> rule4) triple1) -> rule1)) -> rule7) OR ((((((triple1 ((triple1) -> rule2)) -> rule4) triple1) -> rule1)) -> rule7))] Erin is blue.[(((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1))] Harry is blue.[(((((triple7 ((triple7) -> rule2)) -> rule4) triple7) -> rule1))] @4: Dave is big.[(((((((((triple1 triple2) -> rule4) triple1) -> rule1)) -> rule7)) -> rule5) OR ((((((((triple1 ((triple1) -> rule2)) -> rule4) triple1) -> rule1)) -> rule7)) -> rule5))] Erin is cold.[(((((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1)) -> rule7))] @5: Erin is big.[(((((((((triple3 ((triple3) -> rule2)) -> rule4) triple3) -> rule1)) -> rule7)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
((((((triple7 ((triple7) -> (rule2 % int4))) -> (rule4 % int3)) triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((((((triple7 ((triple7) -> (rule2 % int5))) -> (rule4 % int4)) triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
int5
Harry is young.
("Harry" "is" "young" "+")
((triple7) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple1 triple2) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1 triple2) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((((((((triple1 triple2) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
((((((((triple1 ((triple1) -> (rule2 % int5))) -> (rule4 % int4)) triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple3 ((triple3) -> (rule2 % int4))) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((((((triple3 ((triple3) -> (rule2 % int5))) -> (rule4 % int4)) triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5