Dave is big. Dave is kind. Dave is red. Erin is big. Erin is young. Gary is kind. Gary is quiet. Gary is smart. Gary is white. Harry is big. Harry is kind. Harry is quiet. Harry is red. Harry is smart. Harry is white. Harry is young. If something is quiet and smart then it is young.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is quiet and smart then it is young.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Harry is quiet.
True
1
proof
[(triple12)]
("Harry" "is" "quiet" "+")
triple12
Harry is not quiet.
False
1
inv-proof
[(triple12)]
("Harry" "is" "quiet" "-")
triple12
Gary is young.
True
3
proof
[(((triple7 triple8) -> rule1))]
("Gary" "is" "young" "+")
((triple7 triple8) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
3
inv-proof
[(((triple7 triple8) -> rule1))]
("Gary" "is" "young" "-")
((triple7 triple8) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is red.[(triple3)] Erin is big.[(triple4)] Erin is young.[(triple5)] Gary is kind.[(triple6)] Gary is quiet.[(triple7)] Gary is smart.[(triple8)] Gary is white.[(triple9)] Harry is big.[(triple10)] Harry is kind.[(triple11)] Harry is quiet.[(triple12)] Harry is red.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16 OR ((triple12 triple14) -> rule1))] @1: Gary is young.[(((triple7 triple8) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
triple8
Gary is white.
("Gary" "is" "white" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple12 triple14) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple7 triple8) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1