Anne is cold. Anne is green. Bob is cold. Bob is green. Bob is nice. Charlie is cold. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is red. Charlie is smart. Erin is smart. If something is cold then it is smart. If something is cold then it is red. If something is nice and green then it is smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is nice and green then it is smart.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Charlie is cold.
True
1
proof
[(triple6)]
("Charlie" "is" "cold" "+")
triple6
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Bob is smart.
True
2
proof
[(((triple3) -> rule1) OR ((triple5 triple4) -> rule3))]
("Bob" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "red" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Bob is cold.[(triple3)] Bob is green.[(triple4)] Bob is nice.[(triple5)] Charlie is cold.[(triple6)] Charlie is green.[(triple7)] Charlie is nice.[(triple8)] Charlie is quiet.[(triple9)] Charlie is red.[(triple10 OR ((triple6) -> rule2))] Charlie is smart.[(triple11 OR ((triple6) -> rule1) OR ((triple8 triple7) -> rule3))] Erin is smart.[(triple12)] @1: Anne is red.[(((triple1) -> rule2))] Anne is smart.[(((triple1) -> rule1))] Bob is red.[(((triple3) -> rule2))] Bob is smart.[(((triple3) -> rule1) OR ((triple5 triple4) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((triple6) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple8 triple7) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple3) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1