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