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