Anne is big. Anne is not cold. Anne is red. Dave is red. Fiona is furry. Harry is big. Harry is furry. All furry things are blue. Blue things are quiet. If something is red then it is big. If something is red and not cold then it is big. If Anne is furry and Anne is quiet then Anne is blue. If something is furry then it is not red.
Anne is big.
("Anne" "is" "big" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is red.
("Anne" "is" "red" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is red and not cold then it is big.
((("something" "is" "red" "+") ("something" "is" "cold" "~")) -> ("something" "is" "big" "+"))
If Anne is furry and Anne is quiet then Anne is blue.
((("Anne" "is" "furry" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "blue" "+"))
If something is furry then it is not red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "-"))
Anne is big.
True
1
proof
[(triple1 OR ((triple3) -> rule3) OR ((triple3 triple2) -> rule4))]
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple3 triple2) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is not furry.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "furry" "-")
triple5
Fiona is blue.
True
2
proof
[(((triple5) -> rule1))]
("Fiona" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
False
2
inv-proof
[(((triple5) -> rule6))]
("Fiona" "is" "red" "+")
((triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is quiet.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("Fiona" "is" "quiet" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("Harry" "is" "quiet" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is big.[(triple1 OR ((triple3) -> rule3) OR ((triple3 triple2) -> rule4))] Anne is not cold.[(triple2)] Anne is red.[(triple3)] Dave is red.[(triple4)] Fiona is furry.[(triple5)] Harry is big.[(triple6)] Harry is furry.[(triple7)] @1: Dave is big.[(((triple4) -> rule3))] Fiona is blue.[(((triple5) -> rule1))] Fiona is not red.[(((triple5) -> rule6))] Harry is blue.[(((triple7) -> rule1))] Harry is not red.[(((triple7) -> rule6))] @2: Fiona is quiet.[(((((triple5) -> rule1)) -> rule2))] Harry is quiet.[(((((triple7) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple3 triple2) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
((triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((triple7) -> (rule6 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2