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