Charlie is big. Charlie is kind. Charlie is red. Charlie is round. Gary is cold. Gary is green. Gary is red. Harry is big. Harry is cold. Harry is furry. Harry is kind. Harry is round. All red things are green. If Charlie is cold then Charlie is round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Charlie is cold then Charlie is round.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "round" "+"))
Harry is furry.
True
1
proof
[(triple10)]
("Harry" "is" "furry" "+")
triple10
Charlie is not round.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "round" "-")
triple4
Charlie is green.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "green" "+")
((triple3) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "green" "-")
((triple3) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is red.[(triple3)] Charlie is round.[(triple4)] Gary is cold.[(triple5)] Gary is green.[(triple6 OR ((triple7) -> rule1))] Gary is red.[(triple7)] Harry is big.[(triple8)] Harry is cold.[(triple9)] Harry is furry.[(triple10)] Harry is kind.[(triple11)] Harry is round.[(triple12)] @1: Charlie is green.[(((triple3) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
((triple7) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1