Charlie is not big. Charlie is not cold. Charlie is young. Gary is not blue. Gary is not cold. Gary is green. Gary is kind. Gary is white. Harry is blue. Harry is young. If Charlie is big then Charlie is blue. If something is blue then it is big. If something is big then it is cold. If something is young and not cold then it is not green. If something is young and not cold then it is not white. If something is cold then it is white.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
If Charlie is big then Charlie is blue.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "blue" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is young and not cold then it is not green.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "-"))
If something is young and not cold then it is not white.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "-"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Harry is young.
True
1
proof
[(triple10)]
("Harry" "is" "young" "+")
triple10
Charlie is cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not white.
True
3
proof
[(((triple3 triple2) -> rule5))]
("Charlie" "is" "white" "-")
((triple3 triple2) -> (rule5 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is white.
False
3
inv-proof
[(((triple3 triple2) -> rule5))]
("Charlie" "is" "white" "+")
((triple3 triple2) -> (rule5 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Harry is cold.
True
3
proof
[(((((triple9) -> rule2)) -> rule3))]
("Harry" "is" "cold" "+")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule3))]
("Harry" "is" "cold" "-")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
True
4
proof
[(((((((triple9) -> rule2)) -> rule3)) -> rule6))]
("Harry" "is" "white" "+")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not white.
False
4
inv-proof
[(((((((triple9) -> rule2)) -> rule3)) -> rule6))]
("Harry" "is" "white" "-")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is not big.[(triple1)] Charlie is not cold.[(triple2)] Charlie is young.[(triple3)] Gary is green.[(triple6)] Gary is kind.[(triple7)] Gary is not blue.[(triple4)] Gary is not cold.[(triple5)] Gary is white.[(triple8)] Harry is blue.[(triple9)] Harry is young.[(triple10)] @1: Charlie is not green.[(((triple3 triple2) -> rule4))] Charlie is not white.[(((triple3 triple2) -> rule5))] Harry is big.[(((triple9) -> rule2))] @2: Harry is cold.[(((((triple9) -> rule2)) -> rule3))] @3: Harry is white.[(((((((triple9) -> rule2)) -> rule3)) -> rule6))]
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is not blue.
("Gary" "is" "blue" "-")
triple4
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is not green.
("Charlie" "is" "green" "-")
((triple3 triple2) -> (rule4 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is not white.
("Charlie" "is" "white" "-")
((triple3 triple2) -> (rule5 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple9) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3