Anne is big. Anne is blue. Anne is cold. Anne is red. Anne is young. Charlie is big. Charlie is red. Charlie is rough. Charlie is young. Fiona is green. Fiona is red. Fiona is young. If Charlie is rough then Charlie is red. Cold, young people are blue. All green, rough people are big. Red, rough people are cold. If someone is young and green then they are red. Cold people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Charlie is rough then Charlie is red.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "red" "+"))
Cold, young people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All green, rough people are big.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Red, rough people are cold.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is young and green then they are red.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Charlie is big.
True
1
proof
[(triple6 OR ((((((triple7 triple8) -> rule4)) -> rule6) triple8) -> rule3) OR ((((((((triple8) -> rule1) triple8) -> rule4)) -> rule6) triple8) -> rule3))]
("Charlie" "is" "big" "+")
triple6
((((((triple7 triple8) -> (rule4 % int3))) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((((triple8) -> (rule1 % int4)) triple8) -> (rule4 % int3))) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is not young.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "young" "-")
triple9
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple3 triple5) -> rule2))] Anne is cold.[(triple3)] Anne is red.[(triple4 OR ((triple5 ((triple3) -> rule6)) -> rule5))] Anne is young.[(triple5)] Charlie is big.[(triple6 OR ((((((triple7 triple8) -> rule4)) -> rule6) triple8) -> rule3) OR ((((((((triple8) -> rule1) triple8) -> rule4)) -> rule6) triple8) -> rule3))] Charlie is red.[(triple7 OR ((triple8) -> rule1))] Charlie is rough.[(triple8)] Charlie is young.[(triple9)] Fiona is green.[(triple10)] Fiona is red.[(triple11 OR ((triple12 triple10) -> rule5))] Fiona is young.[(triple12)] @1: Anne is green.[(((triple3) -> rule6))] Charlie is cold.[(((triple7 triple8) -> rule4) OR ((((triple8) -> rule1) triple8) -> rule4))] @2: Charlie is blue.[(((((triple7 triple8) -> rule4) triple9) -> rule2) OR ((((((triple8) -> rule1) triple8) -> rule4) triple9) -> rule2))] Charlie is green.[(((((triple7 triple8) -> rule4)) -> rule6) OR ((((((triple8) -> rule1) triple8) -> rule4)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple3 triple5) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple5 ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
((((((triple7 triple8) -> (rule4 % int3))) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((((triple8) -> (rule1 % int4)) triple8) -> (rule4 % int3))) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
triple7
((triple8) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Charlie is young.
("Charlie" "is" "young" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
((triple12 triple10) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple7 triple8) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple7 triple8) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple8) -> (rule1 % int3)) triple8) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((triple7 triple8) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple8) -> (rule1 % int3)) triple8) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3