Bob is green. Bob is kind. Bob is round. Charlie is blue. Charlie is cold. Charlie is red. Erin is big. Erin is cold. Erin is green. Erin is kind. Erin is red. Erin is round. Kind, cold things are round. Green, kind things are red. All green, big things are cold.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Kind, cold things are round.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Green, kind things are red.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All green, big things are cold.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
Erin is cold.
True
1
proof
[(triple8 OR ((triple9 triple7) -> rule3))]
("Erin" "is" "cold" "+")
triple8
((triple9 triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not round.
False
1
inv-proof
[(triple12 OR ((triple10 triple8) -> rule1) OR ((triple10 ((triple9 triple7) -> rule3)) -> rule1))]
("Erin" "is" "round" "-")
triple12
((triple10 triple8) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple10 ((triple9 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is round.[(triple3)] Charlie is blue.[(triple4)] Charlie is cold.[(triple5)] Charlie is red.[(triple6)] Erin is big.[(triple7)] Erin is cold.[(triple8 OR ((triple9 triple7) -> rule3))] Erin is green.[(triple9)] Erin is kind.[(triple10)] Erin is red.[(triple11 OR ((triple9 triple10) -> rule2))] Erin is round.[(triple12 OR ((triple10 triple8) -> rule1) OR ((triple10 ((triple9 triple7) -> rule3)) -> rule1))] @1: Bob is red.[(((triple1 triple2) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple9 triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple9 triple10) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple12
((triple10 triple8) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple10 ((triple9 triple7) -> (rule3 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1