Anne is red. Fiona is kind. Fiona is quiet. If someone is smart then they are kind. If someone is kind and big then they are blue. If Anne is red then Anne is smart. Kind people are cold. Blue people are cold. All red, kind people are cold. Kind, smart people are big. All kind people are quiet.
Anne is red.
("Anne" "is" "red" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and big then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If Anne is red then Anne is smart.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "smart" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All red, kind people are cold.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Kind, smart people are big.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Fiona is kind.
True
1
proof
[(triple2)]
("Fiona" "is" "kind" "+")
triple2
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Anne is smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule8))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not big.
False
6
inv-proof
[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule7))]
("Anne" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is red.[(triple1)] Fiona is kind.[(triple2)] Fiona is quiet.[(triple3 OR ((triple2) -> rule8))] @1: Anne is smart.[(((triple1) -> rule3))] Fiona is cold.[(((triple2) -> rule4))] @2: Anne is kind.[(((((triple1) -> rule3)) -> rule1))] @3: Anne is big.[(((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule7))] Anne is cold.[(((((((triple1) -> rule3)) -> rule1)) -> rule4) OR ((triple1 ((((triple1) -> rule3)) -> rule1)) -> rule6) OR ((((((((triple1) -> rule3)) -> rule1) ((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule7)) -> rule2)) -> rule5))] Anne is quiet.[(((((((triple1) -> rule3)) -> rule1)) -> rule8))] @4: Anne is blue.[(((((((triple1) -> rule3)) -> rule1) ((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule7)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
((triple2) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((((triple1) -> (rule3 % int5))) -> (rule1 % int4)) ((((((triple1) -> (rule3 % int5))) -> (rule1 % int4)) ((triple1) -> (rule3 % int5))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int4))) -> (rule1 % int3)) ((((((triple1) -> (rule3 % int4))) -> (rule1 % int3)) ((triple1) -> (rule3 % int4))) -> (rule7 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4