Anne is green. Anne is young. Bob is green. Bob is young. Charlie is cold. Charlie is quiet. Gary is big. If someone is quiet then they are young. Cold people are quiet. Big people are red. Quiet people are cold. All young people are quiet. Red people are green. Green people are young. All blue, red people are quiet.
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All blue, red people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Anne is young.
True
1
proof
[(triple2 OR ((triple1) -> rule7))]
("Anne" "is" "young" "+")
triple2
((triple1) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Anne is quiet.
True
2
proof
[(((triple2) -> rule5) OR ((((triple1) -> rule7)) -> rule5))]
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not quiet.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple1) -> rule7)) -> rule5))]
("Anne" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is cold.
True
3
proof
[(((((triple4) -> rule5)) -> rule4) OR ((((((triple3) -> rule7)) -> rule5)) -> rule4))]
("Bob" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Gary is not green.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule6))]
("Gary" "is" "green" "-")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
True
4
proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule7))]
("Gary" "is" "young" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not young.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule6)) -> rule7))]
("Gary" "is" "young" "-")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
True
5
proof
[(((((((((triple7) -> rule3)) -> rule6)) -> rule7)) -> rule5))]
("Gary" "is" "quiet" "+")
((((((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is not quiet.
False
5
inv-proof
[(((((((((triple7) -> rule3)) -> rule6)) -> rule7)) -> rule5))]
("Gary" "is" "quiet" "-")
((((((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is cold.
True
6
proof
[(((((((((((triple7) -> rule3)) -> rule6)) -> rule7)) -> rule5)) -> rule4))]
("Gary" "is" "cold" "+")
((((((((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Gary is not cold.
False
6
inv-proof
[(((((((((((triple7) -> rule3)) -> rule6)) -> rule7)) -> rule5)) -> rule4))]
("Gary" "is" "cold" "-")
((((((((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is green.[(triple1)] Anne is young.[(triple2 OR ((triple1) -> rule7))] Bob is green.[(triple3)] Bob is young.[(triple4 OR ((triple3) -> rule7))] Charlie is cold.[(triple5 OR ((triple6) -> rule4))] Charlie is quiet.[(triple6 OR ((triple5) -> rule2))] Gary is big.[(triple7)] @1: Anne is quiet.[(((triple2) -> rule5) OR ((((triple1) -> rule7)) -> rule5))] Bob is quiet.[(((triple4) -> rule5) OR ((((triple3) -> rule7)) -> rule5))] Charlie is young.[(((triple6) -> rule1) OR ((((triple5) -> rule2)) -> rule1))] Gary is red.[(((triple7) -> rule3))] @2: Anne is cold.[(((((triple2) -> rule5)) -> rule4) OR ((((((triple1) -> rule7)) -> rule5)) -> rule4))] Bob is cold.[(((((triple4) -> rule5)) -> rule4) OR ((((((triple3) -> rule7)) -> rule5)) -> rule4))] Gary is green.[(((((triple7) -> rule3)) -> rule6))] @3: Gary is young.[(((((((triple7) -> rule3)) -> rule6)) -> rule7))] @4: Gary is quiet.[(((((((((triple7) -> rule3)) -> rule6)) -> rule7)) -> rule5))] @5: Gary is cold.[(((((((((((triple7) -> rule3)) -> rule6)) -> rule7)) -> rule5)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
((triple1) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple3) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
((triple6) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple5) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple6) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((((((triple7) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5