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