Anne is big. Anne is blue. Anne is red. Erin is blue. Fiona is big. Fiona is furry. Fiona is green. Fiona is kind. Fiona is red. Fiona is smart. If someone is furry and not big then they are not smart. If someone is kind then they are smart. If Anne is blue then Anne is green. If Erin is furry and Erin is big then Erin is green. Green people are kind. All big, smart people are blue. If Erin is big and Erin is not smart then Erin is not blue. If Erin is not smart then Erin is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is furry and not big then they are not smart.
((("someone" "is" "furry" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "smart" "-"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Anne is blue then Anne is green.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "green" "+"))
If Erin is furry and Erin is big then Erin is green.
((("Erin" "is" "furry" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "green" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All big, smart people are blue.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Erin is big and Erin is not smart then Erin is not blue.
((("Erin" "is" "big" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "blue" "-"))
If Erin is not smart then Erin is red.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "red" "+"))
Erin is blue.
True
1
proof
[(triple4)]
("Erin" "is" "blue" "+")
triple4
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is green.
True
2
proof
[(((triple2) -> rule3))]
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Fiona is not blue.
False
3
inv-proof
[(((triple5 triple10) -> rule6) OR ((triple5 ((triple8) -> rule2)) -> rule6) OR ((triple5 ((((triple7) -> rule5)) -> rule2)) -> rule6))]
("Fiona" "is" "blue" "-")
((triple5 triple10) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple5 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple5 ((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Anne is kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Anne" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Anne" "is" "kind" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is not kind.
Unknown
inv-rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not smart.
Unknown
inv-rconc
[@3: Erin is smart.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule4 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is red.[(triple3)] Erin is blue.[(triple4)] Fiona is big.[(triple5)] Fiona is furry.[(triple6)] Fiona is green.[(triple7)] Fiona is kind.[(triple8 OR ((triple7) -> rule5))] Fiona is red.[(triple9)] Fiona is smart.[(triple10 OR ((triple8) -> rule2) OR ((((triple7) -> rule5)) -> rule2))] @1: Anne is green.[(((triple2) -> rule3))] Fiona is blue.[(((triple5 triple10) -> rule6) OR ((triple5 ((triple8) -> rule2)) -> rule6) OR ((triple5 ((((triple7) -> rule5)) -> rule2)) -> rule6))] @2: Anne is kind.[(((((triple2) -> rule3)) -> rule5))] @3: Anne is smart.[(((((((triple2) -> rule3)) -> rule5)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
((triple7) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple8) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5 triple10) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple5 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple5 ((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3