Anne is cold. Anne is not young. Fiona is furry. Fiona is nice. Gary is smart. Gary is young. Harry is not cold. Harry is furry. Harry is smart. Harry is young. If something is smart then it is red. Smart things are red. If something is young and red then it is not nice. All cold things are furry. If something is smart and not nice then it is furry. If something is furry then it is green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not young.
("Anne" "is" "young" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is young and red then it is not nice.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is smart and not nice then it is furry.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "furry" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Fiona is furry.
True
1
proof
[(triple3)]
("Fiona" "is" "furry" "+")
triple3
Gary is not smart.
False
1
inv-proof
[(triple5)]
("Gary" "is" "smart" "-")
triple5
Anne is furry.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple3) -> rule6))]
("Fiona" "is" "green" "-")
((triple3) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is not nice.
True
4
proof
[(((triple6 ((triple5) -> rule1)) -> rule3) OR ((triple6 ((triple5) -> rule2)) -> rule3))]
("Gary" "is" "nice" "-")
((triple6 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple6 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is nice.
False
4
inv-proof
[(((triple10 ((triple9) -> rule1)) -> rule3) OR ((triple10 ((triple9) -> rule2)) -> rule3))]
("Harry" "is" "nice" "+")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple10 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is furry.
True
6
proof
[(((triple5 ((triple6 ((triple5) -> rule1)) -> rule3)) -> rule5) OR ((triple5 ((triple6 ((triple5) -> rule2)) -> rule3)) -> rule5))]
("Gary" "is" "furry" "+")
((triple5 ((triple6 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((triple5 ((triple6 ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not furry.
False
6
inv-proof
[(((triple5 ((triple6 ((triple5) -> rule1)) -> rule3)) -> rule5) OR ((triple5 ((triple6 ((triple5) -> rule2)) -> rule3)) -> rule5))]
("Gary" "is" "furry" "-")
((triple5 ((triple6 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((triple5 ((triple6 ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is not young.[(triple2)] Fiona is furry.[(triple3)] Fiona is nice.[(triple4)] Gary is smart.[(triple5)] Gary is young.[(triple6)] Harry is furry.[(triple8 OR ((triple9 ((triple10 ((triple9) -> rule1)) -> rule3)) -> rule5) OR ((triple9 ((triple10 ((triple9) -> rule2)) -> rule3)) -> rule5))] Harry is not cold.[(triple7)] Harry is smart.[(triple9)] Harry is young.[(triple10)] @1: Anne is furry.[(((triple1) -> rule4))] Fiona is green.[(((triple3) -> rule6))] Gary is red.[(((triple5) -> rule1) OR ((triple5) -> rule2))] Harry is green.[(((triple8) -> rule6) OR ((((triple9 ((triple10 ((triple9) -> rule1)) -> rule3)) -> rule5)) -> rule6) OR ((((triple9 ((triple10 ((triple9) -> rule2)) -> rule3)) -> rule5)) -> rule6))] Harry is red.[(((triple9) -> rule1) OR ((triple9) -> rule2))] @2: Anne is green.[(((((triple1) -> rule4)) -> rule6))] Gary is not nice.[(((triple6 ((triple5) -> rule1)) -> rule3) OR ((triple6 ((triple5) -> rule2)) -> rule3))] Harry is not nice.[(((triple10 ((triple9) -> rule1)) -> rule3) OR ((triple10 ((triple9) -> rule2)) -> rule3))] @3: Gary is furry.[(((triple5 ((triple6 ((triple5) -> rule1)) -> rule3)) -> rule5) OR ((triple5 ((triple6 ((triple5) -> rule2)) -> rule3)) -> rule5))] @4: Gary is green.[(((((triple5 ((triple6 ((triple5) -> rule1)) -> rule3)) -> rule5)) -> rule6) OR ((((triple5 ((triple6 ((triple5) -> rule2)) -> rule3)) -> rule5)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not young.
("Anne" "is" "young" "-")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Gary is young.
("Gary" "is" "young" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple9 ((triple10 ((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((triple9 ((triple10 ((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not cold.
("Harry" "is" "cold" "-")
triple7
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple5) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple5) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple8) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple9 ((triple10 ((triple9) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
((((triple9 ((triple10 ((triple9) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
((triple9) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple9) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((triple6 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple6 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple10 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple5 ((triple6 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((triple5 ((triple6 ((triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((triple5 ((triple6 ((triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((triple5 ((triple6 ((triple5) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Gary is red.
("Gary" "is" "red" "+")
int4