Charlie is cold. Charlie is young. Gary is cold. If Gary is nice and Gary is red then Gary is cold. All young, cold things are white. Nice things are young. All big things are red. If Charlie is white then Charlie is nice. Cold things are nice. If Gary is young then Gary is white. If something is big and kind then it is young.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If Gary is nice and Gary is red then Gary is cold.
((("Gary" "is" "nice" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "cold" "+"))
All young, cold things are white.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If Charlie is white then Charlie is nice.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "nice" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Gary is young then Gary is white.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "white" "+"))
If something is big and kind then it is young.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Charlie is young.
True
1
proof
[(triple2 OR ((((triple1) -> rule6)) -> rule3))]
("Charlie" "is" "young" "+")
triple2
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Charlie is nice.
True
2
proof
[(((triple1) -> rule6) OR ((((triple2 triple1) -> rule2)) -> rule5))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is not nice.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "nice" "-")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("Gary" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("Gary" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule7) OR ((((((triple3) -> rule6)) -> rule3) triple3) -> rule2))]
("Gary" "is" "white" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule7) OR ((((((triple3) -> rule6)) -> rule3) triple3) -> rule2))]
("Gary" "is" "white" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "red" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is cold.[(triple1)] Charlie is young.[(triple2 OR ((((triple1) -> rule6)) -> rule3))] Gary is cold.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule6) OR ((((triple2 triple1) -> rule2)) -> rule5))] Charlie is white.[(((triple2 triple1) -> rule2) OR ((((((triple1) -> rule6)) -> rule3) triple1) -> rule2))] Gary is nice.[(((triple3) -> rule6))] @2: Gary is young.[(((((triple3) -> rule6)) -> rule3))] @3: Gary is white.[(((((((triple3) -> rule6)) -> rule3)) -> rule7) OR ((((((triple3) -> rule6)) -> rule3) triple3) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2 triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3