Dave is big. Dave is blue. Dave is cold. Dave is red. Dave is rough. Dave is smart. Gary is big. Gary is cold. Gary is nice. Gary is rough. If someone is blue and nice then they are cold. Smart, nice people are blue. Smart, blue people are red. If Gary is smart and Gary is rough then Gary is big. If Gary is smart then Gary is rough. If Gary is nice then Gary is big. If someone is big then they are red. Red people are cold.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is blue and nice then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Smart, nice people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Smart, blue people are red.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If Gary is smart and Gary is rough then Gary is big.
((("Gary" "is" "smart" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "big" "+"))
If Gary is smart then Gary is rough.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is nice then Gary is big.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "big" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple6)]
("Dave" "is" "smart" "+")
triple6
Dave is not cold.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((triple6 triple2) -> rule3)) -> rule8))]
("Dave" "is" "cold" "-")
triple3
((triple4) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple6 triple2) -> (rule3 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is cold.[(triple3 OR ((triple4) -> rule8) OR ((((triple1) -> rule7)) -> rule8) OR ((((triple6 triple2) -> rule3)) -> rule8))] Dave is red.[(triple4 OR ((triple1) -> rule7) OR ((triple6 triple2) -> rule3))] Dave is rough.[(triple5)] Dave is smart.[(triple6)] Gary is big.[(triple7 OR ((triple9) -> rule6))] Gary is cold.[(triple8 OR ((((triple7) -> rule7)) -> rule8) OR ((((((triple9) -> rule6)) -> rule7)) -> rule8))] Gary is nice.[(triple9)] Gary is rough.[(triple10)] @1: Gary is red.[(((triple7) -> rule7) OR ((((triple9) -> rule6)) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((triple4) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple6 triple2) -> (rule3 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple1) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple6 triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple9) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2