Charlie is cold. Charlie is rough. Charlie is smart. Gary is blue. Gary is cold. Harry is blue. Harry is cold. Harry is nice. Harry is rough. Harry is white. White, smart things are rough. If something is cold then it is nice. If something is white and cold then it is young. If Harry is smart then Harry is rough. Nice things are white. All rough, blue things are white.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
White, smart things are rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is white and cold then it is young.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Harry is smart then Harry is rough.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
All rough, blue things are white.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple8 OR ((triple7) -> rule2))]
("Harry" "is" "nice" "+")
triple8
((triple7) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not white.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule5) OR ((triple9 triple6) -> rule6) OR ((((triple7) -> rule2)) -> rule5))]
("Harry" "is" "white" "-")
triple10
((triple8) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 triple6) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
True
3
proof
[(((triple10 triple7) -> rule3) OR ((((triple8) -> rule5) triple7) -> rule3) OR ((((triple9 triple6) -> rule6) triple7) -> rule3) OR ((((((triple7) -> rule2)) -> rule5) triple7) -> rule3))]
("Harry" "is" "young" "+")
((triple10 triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple8) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple9 triple6) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Gary is not nice.
False
2
inv-proof
[(((triple5) -> rule2))]
("Gary" "is" "nice" "-")
((triple5) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
True
3
proof
[(((((triple5) -> rule2)) -> rule5))]
("Gary" "is" "white" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is young.
True
5
proof
[(((((((triple5) -> rule2)) -> rule5) triple5) -> rule3))]
("Gary" "is" "young" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not young.
False
5
inv-proof
[(((((((triple5) -> rule2)) -> rule5) triple5) -> rule3))]
("Gary" "is" "young" "-")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Charlie is cold.[(triple1)] Charlie is rough.[(triple2 OR ((((((triple1) -> rule2)) -> rule5) triple3) -> rule1))] Charlie is smart.[(triple3)] Gary is blue.[(triple4)] Gary is cold.[(triple5)] Harry is blue.[(triple6)] Harry is cold.[(triple7)] Harry is nice.[(triple8 OR ((triple7) -> rule2))] Harry is rough.[(triple9)] Harry is white.[(triple10 OR ((triple8) -> rule5) OR ((triple9 triple6) -> rule6) OR ((((triple7) -> rule2)) -> rule5))] @1: Charlie is nice.[(((triple1) -> rule2))] Gary is nice.[(((triple5) -> rule2))] Harry is young.[(((triple10 triple7) -> rule3) OR ((((triple8) -> rule5) triple7) -> rule3) OR ((((triple9 triple6) -> rule6) triple7) -> rule3) OR ((((((triple7) -> rule2)) -> rule5) triple7) -> rule3))] @2: Charlie is white.[(((((triple1) -> rule2)) -> rule5))] Gary is white.[(((((triple5) -> rule2)) -> rule5))] @3: Charlie is young.[(((((((triple1) -> rule2)) -> rule5) triple1) -> rule3))] Gary is young.[(((((((triple5) -> rule2)) -> rule5) triple5) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple7) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple8) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple9 triple6) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple5) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10 triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple8) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple9 triple6) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule5 % int2)) triple7) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2)) triple5) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3