Bob is red. Bob is rough. Dave is big. Dave is blue. Dave is cold. Dave is kind. Dave is nice. Dave is red. Dave is rough. Erin is big. Erin is cold. Erin is nice. Erin is rough. Gary is big. Gary is cold. Gary is kind. Cold things are blue. Rough things are cold.
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Gary is cold.
True
1
proof
[(triple15)]
("Gary" "is" "cold" "+")
triple15
Dave is not blue.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule1) OR ((((triple9) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
triple4
((triple5) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is blue.
True
2
proof
[(((triple11) -> rule1) OR ((((triple13) -> rule2)) -> rule1))]
("Erin" "is" "blue" "+")
((triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is not blue.
False
2
inv-proof
[(((triple15) -> rule1))]
("Gary" "is" "blue" "-")
((triple15) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is blue.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "blue" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is red.[(triple1)] Bob is rough.[(triple2)] Dave is big.[(triple3)] Dave is blue.[(triple4 OR ((triple5) -> rule1) OR ((((triple9) -> rule2)) -> rule1))] Dave is cold.[(triple5 OR ((triple9) -> rule2))] Dave is kind.[(triple6)] Dave is nice.[(triple7)] Dave is red.[(triple8)] Dave is rough.[(triple9)] Erin is big.[(triple10)] Erin is cold.[(triple11 OR ((triple13) -> rule2))] Erin is nice.[(triple12)] Erin is rough.[(triple13)] Gary is big.[(triple14)] Gary is cold.[(triple15)] Gary is kind.[(triple16)] @1: Bob is cold.[(((triple2) -> rule2))] Erin is blue.[(((triple11) -> rule1) OR ((((triple13) -> rule2)) -> rule1))] Gary is blue.[(((triple15) -> rule1))] @2: Bob is blue.[(((((triple2) -> rule2)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is cold.
("Erin" "is" "cold" "+")
triple11
((triple13) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
Gary is big.
("Gary" "is" "big" "+")
triple14
Gary is cold.
("Gary" "is" "cold" "+")
triple15
Gary is kind.
("Gary" "is" "kind" "+")
triple16
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple15) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2