Anne is big. Anne is blue. Anne is kind. Anne is quiet. Anne is smart. Erin is blue. Erin is cold. Erin is kind. Erin is quiet. Fiona is big. Fiona is blue. Fiona is cold. Gary is kind. Gary is quiet. Gary is smart. If someone is big then they are cold. Blue people are smart. If Fiona is blue and Fiona is big then Fiona is quiet. All smart people are kind. All kind people are quiet. If someone is smart and big then they are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is blue and Fiona is big then Fiona is quiet.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "big" "+")) -> ("Fiona" "is" "quiet" "+"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and big then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
Anne is smart.
True
1
proof
[(triple5 OR ((triple2) -> rule2))]
("Anne" "is" "smart" "+")
triple5
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule2))]
("Anne" "is" "smart" "-")
triple5
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple6) -> rule2))]
("Erin" "is" "smart" "-")
((triple6) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is kind.
True
3
proof
[(((((triple11) -> rule2)) -> rule4))]
("Fiona" "is" "kind" "+")
((((triple11) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not kind.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule4))]
("Fiona" "is" "kind" "-")
((((triple11) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is kind.[(triple3 OR ((triple5) -> rule4) OR ((((triple2) -> rule2)) -> rule4))] Anne is quiet.[(triple4 OR ((triple3) -> rule5) OR ((triple5 triple1) -> rule6) OR ((((triple5) -> rule4)) -> rule5) OR ((((triple2) -> rule2) triple1) -> rule6) OR ((((((triple2) -> rule2)) -> rule4)) -> rule5))] Anne is smart.[(triple5 OR ((triple2) -> rule2))] Erin is blue.[(triple6)] Erin is cold.[(triple7)] Erin is kind.[(triple8 OR ((((triple6) -> rule2)) -> rule4))] Erin is quiet.[(triple9 OR ((triple8) -> rule5) OR ((((((triple6) -> rule2)) -> rule4)) -> rule5))] Fiona is big.[(triple10)] Fiona is blue.[(triple11)] Fiona is cold.[(triple12 OR ((triple10) -> rule1))] Gary is kind.[(triple13 OR ((triple15) -> rule4))] Gary is quiet.[(triple14 OR ((triple13) -> rule5) OR ((((triple15) -> rule4)) -> rule5))] Gary is smart.[(triple15)] @1: Anne is cold.[(((triple1) -> rule1))] Erin is smart.[(((triple6) -> rule2))] Fiona is quiet.[(((triple11 triple10) -> rule3) OR ((((triple11) -> rule2) triple10) -> rule6) OR ((((((triple11) -> rule2)) -> rule4)) -> rule5))] Fiona is smart.[(((triple11) -> rule2))] @2: Fiona is kind.[(((((triple11) -> rule2)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple5) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
((triple3) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple5 triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple5
((triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple8) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((((triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
triple10
Fiona is blue.
("Fiona" "is" "blue" "+")
triple11
Fiona is cold.
("Fiona" "is" "cold" "+")
triple12
((triple10) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple13
((triple15) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
((triple13) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple15) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple11 triple10) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple11) -> (rule2 % int2)) triple10) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple11) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple11) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple11) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2