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