Bob is green. Bob is red. Dave is green. Dave is red. Erin is cold. Erin is green. Erin is rough. Erin is white. Harry is big. Harry is cold. Harry is red. Harry is rough. Red things are cold.
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple10 OR ((triple11) -> rule1))]
("Harry" "is" "cold" "+")
triple10
((triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Erin is not white.
False
1
inv-proof
[(triple8)]
("Erin" "is" "white" "-")
triple8
Dave is cold.
True
2
proof
[(((triple4) -> rule1))]
("Dave" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Bob is green.[(triple1)] Bob is red.[(triple2)] Dave is green.[(triple3)] Dave is red.[(triple4)] Erin is cold.[(triple5)] Erin is green.[(triple6)] Erin is rough.[(triple7)] Erin is white.[(triple8)] Harry is big.[(triple9)] Harry is cold.[(triple10 OR ((triple11) -> rule1))] Harry is red.[(triple11)] Harry is rough.[(triple12)] @1: Bob is cold.[(((triple2) -> rule1))] Dave is cold.[(((triple4) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1