Anne is kind. Anne is round. Bob is blue. Bob is smart. Fiona is young. Gary is cold. Gary is not red. Gary is round. Gary is not smart. Gary is not young. If someone is blue and round then they are red. If someone is blue and young then they are red. All red people are cold. If someone is red then they are young. If someone is kind then they are blue. All young people are kind. Cold people are round.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is round.
("Gary" "is" "round" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is not young.
("Gary" "is" "young" "-")
If someone is blue and round then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and young then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Gary is cold.
True
1
proof
[(triple6)]
("Gary" "is" "cold" "+")
triple6
Gary is young.
False
1
inv-proof
[(triple10)]
("Gary" "is" "young" "+")
triple10
Fiona is kind.
True
2
proof
[(((triple5) -> rule6))]
("Fiona" "is" "kind" "+")
((triple5) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple5) -> rule6))]
("Fiona" "is" "kind" "-")
((triple5) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Anne is red.
True
4
proof
[(((((triple1) -> rule5) triple2) -> rule1))]
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1) -> rule5) triple2) -> rule1))]
("Anne" "is" "red" "-")
((((triple1) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
True
5
proof
[(((((((triple1) -> rule5) triple2) -> rule1)) -> rule3))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Fiona is not red.
False
5
inv-proof
[(((((((triple5) -> rule6)) -> rule5) triple5) -> rule2))]
("Fiona" "is" "red" "-")
((((((triple5) -> (rule6 % int3))) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is cold.
True
6
proof
[(((((((((triple5) -> rule6)) -> rule5) triple5) -> rule2)) -> rule3))]
("Fiona" "is" "cold" "+")
((((((((triple5) -> (rule6 % int4))) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is not cold.
False
6
inv-proof
[(((((((((triple5) -> rule6)) -> rule5) triple5) -> rule2)) -> rule3))]
("Fiona" "is" "cold" "-")
((((((((triple5) -> (rule6 % int4))) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is round.
True
7
proof
[(((((((((((triple5) -> rule6)) -> rule5) triple5) -> rule2)) -> rule3)) -> rule7))]
("Fiona" "is" "round" "+")
((((((((((triple5) -> (rule6 % int5))) -> (rule5 % int4)) triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Fiona is not round.
False
7
inv-proof
[(((((((((((triple5) -> rule6)) -> rule5) triple5) -> rule2)) -> rule3)) -> rule7))]
("Fiona" "is" "round" "-")
((((((((((triple5) -> (rule6 % int5))) -> (rule5 % int4)) triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Bob is not red.
Unknown
inv-rconc
[@5: Bob is red.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule3 <- rule2 <- rule4 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@6: Bob is kind.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule1 <- rule7 <- rule3 <- rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is cold.
Unknown
rconc
[@5: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule4 <- rule1 <- rule7 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not young.
Unknown
inv-rconc
[@5: Bob is young.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- rule3 <- rule2 <- FAIL)]]
("Bob" "is" "young" "-")
Gary is blue.
Unknown
rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Gary" "is" "blue" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Anne is round.[(triple2)] Bob is blue.[(triple3)] Bob is smart.[(triple4)] Fiona is young.[(triple5)] Gary is cold.[(triple6)] Gary is not red.[(triple7)] Gary is not smart.[(triple9)] Gary is not young.[(triple10)] Gary is round.[(triple8 OR ((triple6) -> rule7))] @1: Anne is blue.[(((triple1) -> rule5))] Fiona is kind.[(((triple5) -> rule6))] @2: Anne is red.[(((((triple1) -> rule5) triple2) -> rule1))] Fiona is blue.[(((((triple5) -> rule6)) -> rule5))] @3: Anne is cold.[(((((((triple1) -> rule5) triple2) -> rule1)) -> rule3))] Anne is young.[(((((((triple1) -> rule5) triple2) -> rule1)) -> rule4))] Fiona is red.[(((((((triple5) -> rule6)) -> rule5) triple5) -> rule2))] @4: Fiona is cold.[(((((((((triple5) -> rule6)) -> rule5) triple5) -> rule2)) -> rule3))] @5: Fiona is round.[(((((((((((triple5) -> rule6)) -> rule5) triple5) -> rule2)) -> rule3)) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is not red.
("Gary" "is" "red" "-")
triple7
Gary is not smart.
("Gary" "is" "smart" "-")
triple9
Gary is not young.
("Gary" "is" "young" "-")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple8
((triple6) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule5 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
((((((triple5) -> (rule6 % int3))) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((((triple5) -> (rule6 % int4))) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
((((((((((triple5) -> (rule6 % int5))) -> (rule5 % int4)) triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5