Anne is cold. Charlie is furry. Charlie is quiet. Erin is cold. Erin is young. Gary is smart. Gary is young. If Erin is quiet and Erin is cold then Erin is smart. If something is red and cold then it is quiet. Young, smart things are furry. If something is cold and young then it is red. All cold things are red. If something is smart and not young then it is red. All furry, cold things are blue.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Erin is quiet and Erin is cold then Erin is smart.
((("Erin" "is" "quiet" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "smart" "+"))
If something is red and cold then it is quiet.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Young, smart things are furry.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is cold and young then it is red.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is smart and not young then it is red.
((("something" "is" "smart" "+") ("something" "is" "young" "~")) -> ("something" "is" "red" "+"))
All furry, cold things are blue.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Charlie is not quiet.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Erin is red.
True
2
proof
[(((triple4) -> rule5) OR ((triple4 triple5) -> rule4))]
("Erin" "is" "red" "+")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple4 triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple4) -> rule5) OR ((triple4 triple5) -> rule4))]
("Erin" "is" "red" "-")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple4 triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
True
4
proof
[(((((triple4) -> rule5) triple4) -> rule2) OR ((((triple4 triple5) -> rule4) triple4) -> rule2))]
("Erin" "is" "quiet" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple4 triple5) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple4) -> rule5) triple4) -> rule2) OR ((((triple4 triple5) -> rule4) triple4) -> rule2))]
("Erin" "is" "quiet" "-")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple4 triple5) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
True
6
proof
[(((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1) OR ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1))]
("Erin" "is" "smart" "+")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple4 triple5) -> (rule4 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1) OR ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1))]
("Erin" "is" "smart" "-")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple4 triple5) -> (rule4 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is furry.
True
8
proof
[(((triple5 ((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1)) -> rule3) OR ((triple5 ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1)) -> rule3))]
("Erin" "is" "furry" "+")
((triple5 ((((((triple4) -> (rule5 % int4)) triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((triple5 ((((((triple4 triple5) -> (rule4 % int4)) triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is not furry.
False
8
inv-proof
[(((triple5 ((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1)) -> rule3) OR ((triple5 ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1)) -> rule3))]
("Erin" "is" "furry" "-")
((triple5 ((((((triple4) -> (rule5 % int4)) triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((triple5 ((((((triple4 triple5) -> (rule4 % int4)) triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is blue.
True
10
proof
[(((((triple5 ((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1)) -> rule3) triple4) -> rule7) OR ((((triple5 ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1)) -> rule3) triple4) -> rule7))]
("Erin" "is" "blue" "+")
((((triple5 ((((((triple4) -> (rule5 % int5)) triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
((((triple5 ((((((triple4 triple5) -> (rule4 % int5)) triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Erin is not blue.
False
10
inv-proof
[(((((triple5 ((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1)) -> rule3) triple4) -> rule7) OR ((((triple5 ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1)) -> rule3) triple4) -> rule7))]
("Erin" "is" "blue" "-")
((((triple5 ((((((triple4) -> (rule5 % int5)) triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
((((triple5 ((((((triple4 triple5) -> (rule4 % int5)) triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "blue" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is quiet.[(triple3)] Erin is cold.[(triple4)] Erin is young.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7)] @1: Anne is red.[(((triple1) -> rule5))] Erin is red.[(((triple4) -> rule5) OR ((triple4 triple5) -> rule4))] Gary is furry.[(((triple7 triple6) -> rule3))] @2: Anne is quiet.[(((((triple1) -> rule5) triple1) -> rule2))] Erin is quiet.[(((((triple4) -> rule5) triple4) -> rule2) OR ((((triple4 triple5) -> rule4) triple4) -> rule2))] @3: Erin is smart.[(((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1) OR ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1))] @4: Erin is furry.[(((triple5 ((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1)) -> rule3) OR ((triple5 ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1)) -> rule3))] @5: Erin is blue.[(((((triple5 ((((((triple4) -> rule5) triple4) -> rule2) triple4) -> rule1)) -> rule3) triple4) -> rule7) OR ((((triple5 ((((((triple4 triple5) -> rule4) triple4) -> rule2) triple4) -> rule1)) -> rule3) triple4) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple4 triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple7 triple6) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple4 triple5) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple4 triple5) -> (rule4 % int3)) triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((triple5 ((((((triple4) -> (rule5 % int4)) triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
((triple5 ((((((triple4 triple5) -> (rule4 % int4)) triple4) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((((triple5 ((((((triple4) -> (rule5 % int5)) triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5
((((triple5 ((((((triple4 triple5) -> (rule4 % int5)) triple4) -> (rule2 % int4)) triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
int5