Anne is nice. Gary is green. Gary is nice. Gary is quiet. Gary is smart. Harry is big. Harry is young. If Gary is green and Gary is nice then Gary is quiet. If Harry is young and Harry is smart then Harry is nice. If Gary is nice and Gary is quiet then Gary is smart. All quiet, blue people are smart. If someone is quiet and green then they are blue. If someone is quiet and big then they are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
If Gary is green and Gary is nice then Gary is quiet.
((("Gary" "is" "green" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "quiet" "+"))
If Harry is young and Harry is smart then Harry is nice.
((("Harry" "is" "young" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "nice" "+"))
If Gary is nice and Gary is quiet then Gary is smart.
((("Gary" "is" "nice" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "+"))
All quiet, blue people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet and green then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and big then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Gary is not smart.
False
1
inv-proof
[(triple5 OR ((triple3 triple4) -> rule3) OR ((triple3 ((triple2 triple3) -> rule1)) -> rule3) OR ((triple4 ((triple4 triple2) -> rule5)) -> rule4) OR ((((triple2 triple3) -> rule1) ((triple4 triple2) -> rule5)) -> rule4) OR ((triple4 ((((triple2 triple3) -> rule1) triple2) -> rule5)) -> rule4) OR ((((triple2 triple3) -> rule1) ((((triple2 triple3) -> rule1) triple2) -> rule5)) -> rule4))]
("Gary" "is" "smart" "-")
triple5
((triple3 triple4) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple4 ((triple4 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple2 triple3) -> (rule1 % int3)) ((triple4 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple4 ((((triple2 triple3) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple2 triple3) -> (rule1 % int3)) ((((triple2 triple3) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
True
3
proof
[(((triple4 triple2) -> rule5) OR ((((triple2 triple3) -> rule1) triple2) -> rule5))]
("Gary" "is" "blue" "+")
((triple4 triple2) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((triple4 triple2) -> rule5) OR ((((triple2 triple3) -> rule1) triple2) -> rule5))]
("Gary" "is" "blue" "-")
((triple4 triple2) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "smart" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Gary is green.[(triple2)] Gary is nice.[(triple3)] Gary is quiet.[(triple4 OR ((triple2 triple3) -> rule1))] Gary is smart.[(triple5 OR ((triple3 triple4) -> rule3) OR ((triple3 ((triple2 triple3) -> rule1)) -> rule3) OR ((triple4 ((triple4 triple2) -> rule5)) -> rule4) OR ((((triple2 triple3) -> rule1) ((triple4 triple2) -> rule5)) -> rule4) OR ((triple4 ((((triple2 triple3) -> rule1) triple2) -> rule5)) -> rule4) OR ((((triple2 triple3) -> rule1) ((((triple2 triple3) -> rule1) triple2) -> rule5)) -> rule4))] Harry is big.[(triple6)] Harry is young.[(triple7)] @1: Gary is blue.[(((triple4 triple2) -> rule5) OR ((((triple2 triple3) -> rule1) triple2) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
((triple2 triple3) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple5
((triple3 triple4) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple3 ((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple4 ((triple4 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple2 triple3) -> (rule1 % int3)) ((triple4 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple4 ((((triple2 triple3) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((triple2 triple3) -> (rule1 % int3)) ((((triple2 triple3) -> (rule1 % int3)) triple2) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple4 triple2) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple2 triple3) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2