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