Erin is red. Erin is smart. Gary is blue. Gary is green. Gary is quiet. Gary is rough. Gary is smart. If something is blue and rough then it is big. Red, big things are smart. If Gary is big then Gary is smart.
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is blue and rough then it is big.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Red, big things are smart.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If Gary is big then Gary is smart.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple7 OR ((((triple3 triple6) -> rule1)) -> rule3))]
("Gary" "is" "smart" "+")
triple7
((((triple3 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not quiet.
False
1
inv-proof
[(triple5)]
("Gary" "is" "quiet" "-")
triple5
Gary is big.
True
3
proof
[(((triple3 triple6) -> rule1))]
("Gary" "is" "big" "+")
((triple3 triple6) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
3
inv-proof
[(((triple3 triple6) -> rule1))]
("Gary" "is" "big" "-")
((triple3 triple6) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Erin is red.[(triple1)] Erin is smart.[(triple2)] Gary is blue.[(triple3)] Gary is green.[(triple4)] Gary is quiet.[(triple5)] Gary is rough.[(triple6)] Gary is smart.[(triple7 OR ((((triple3 triple6) -> rule1)) -> rule3))] @1: Gary is big.[(((triple3 triple6) -> rule1))]
Erin is red.
("Erin" "is" "red" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((((triple3 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple3 triple6) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1