Charlie is cold. Charlie is nice. Charlie is red. Charlie is round. Charlie is smart. Gary is cold. Gary is kind. Gary is quiet. Gary is smart. Harry is smart. If Gary is quiet then Gary is smart. All smart people are cold. Quiet people are round.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Gary is quiet then Gary is smart.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Gary is smart.
True
1
proof
[(triple9 OR ((triple8) -> rule1))]
("Gary" "is" "smart" "+")
triple9
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Harry is cold.
True
2
proof
[(((triple10) -> rule2))]
("Harry" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple8) -> rule3))]
("Gary" "is" "round" "-")
((triple8) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Charlie is cold.[(triple1 OR ((triple5) -> rule2))] Charlie is nice.[(triple2)] Charlie is red.[(triple3)] Charlie is round.[(triple4)] Charlie is smart.[(triple5)] Gary is cold.[(triple6 OR ((triple9) -> rule2) OR ((((triple8) -> rule1)) -> rule2))] Gary is kind.[(triple7)] Gary is quiet.[(triple8)] Gary is smart.[(triple9 OR ((triple8) -> rule1))] Harry is smart.[(triple10)] @1: Gary is round.[(((triple8) -> rule3))] Harry is cold.[(((triple10) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple5) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
((triple9) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple8) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
((triple8) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1