Anne is big. Anne is cold. Anne is kind. Anne is rough. Bob is big. Bob is cold. Bob is white. Bob is young. Charlie is white. Erin is big. Erin is furry. Erin is white. If Bob is cold and Bob is rough then Bob is big. If something is big and cold then it is young. If Erin is big then Erin is furry. Furry, young things are white. Cold things are young. If something is furry and kind then it is white. All young things are cold. If something is furry and white then it is kind.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is white.
("Erin" "is" "white" "+")
If Bob is cold and Bob is rough then Bob is big.
((("Bob" "is" "cold" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "big" "+"))
If something is big and cold then it is young.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Erin is big then Erin is furry.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "furry" "+"))
Furry, young things are white.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is furry and kind then it is white.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is furry and white then it is kind.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Bob is cold.
True
1
proof
[(triple6 OR ((triple8) -> rule7))]
("Bob" "is" "cold" "+")
triple6
((triple8) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule7))]
("Bob" "is" "cold" "-")
triple6
((triple8) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is kind.
True
3
proof
[(((triple11 triple12) -> rule8) OR ((((triple10) -> rule3) triple12) -> rule8))]
("Erin" "is" "kind" "+")
((triple11 triple12) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple10) -> (rule3 % int2)) triple12) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is not young.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple1 triple2) -> rule2))]
("Anne" "is" "young" "-")
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "kind" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is rough.[(triple4)] Bob is big.[(triple5)] Bob is cold.[(triple6 OR ((triple8) -> rule7))] Bob is white.[(triple7)] Bob is young.[(triple8 OR ((triple6) -> rule5) OR ((triple5 triple6) -> rule2))] Charlie is white.[(triple9)] Erin is big.[(triple10)] Erin is furry.[(triple11 OR ((triple10) -> rule3))] Erin is white.[(triple12)] @1: Anne is young.[(((triple2) -> rule5) OR ((triple1 triple2) -> rule2))] Erin is kind.[(((triple11 triple12) -> rule8) OR ((((triple10) -> rule3) triple12) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is cold.
("Bob" "is" "cold" "+")
triple6
((triple8) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
((triple6) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple6) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is furry.
("Erin" "is" "furry" "+")
triple11
((triple10) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple12
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple11 triple12) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple10) -> (rule3 % int2)) triple12) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2