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