Charlie is red. Charlie is smart. Erin is quiet. Erin is red. Erin is rough. Erin is smart. Gary is furry. Gary is kind. Gary is quiet. Gary is red. Gary is rough. Gary is smart. Harry is red. Harry is smart. Harry is young. Red, young things are furry. All furry, kind things are smart. If something is smart and quiet then it is young.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Red, young things are furry.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All furry, kind things are smart.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is smart and quiet then it is young.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Gary is smart.
True
1
proof
[(triple12 OR ((triple7 triple8) -> rule2))]
("Gary" "is" "smart" "+")
triple12
((triple7 triple8) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not quiet.
False
1
inv-proof
[(triple9)]
("Gary" "is" "quiet" "-")
triple9
Gary is young.
True
3
proof
[(((triple12 triple9) -> rule3) OR ((((triple7 triple8) -> rule2) triple9) -> rule3))]
("Gary" "is" "young" "+")
((triple12 triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((triple13 triple15) -> rule1))]
("Harry" "is" "furry" "-")
((triple13 triple15) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is furry.
True
5
proof
[(((triple4 ((triple6 triple3) -> rule3)) -> rule1))]
("Erin" "is" "furry" "+")
((triple4 ((triple6 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not furry.
False
5
inv-proof
[(((triple4 ((triple6 triple3) -> rule3)) -> rule1))]
("Erin" "is" "furry" "-")
((triple4 ((triple6 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "furry" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is red.[(triple1)] Charlie is smart.[(triple2)] Erin is quiet.[(triple3)] Erin is red.[(triple4)] Erin is rough.[(triple5)] Erin is smart.[(triple6)] Gary is furry.[(triple7 OR ((triple10 ((triple12 triple9) -> rule3)) -> rule1))] Gary is kind.[(triple8)] Gary is quiet.[(triple9)] Gary is red.[(triple10)] Gary is rough.[(triple11)] Gary is smart.[(triple12 OR ((triple7 triple8) -> rule2))] Harry is red.[(triple13)] Harry is smart.[(triple14)] Harry is young.[(triple15)] @1: Erin is young.[(((triple6 triple3) -> rule3))] Gary is young.[(((triple12 triple9) -> rule3) OR ((((triple7 triple8) -> rule2) triple9) -> rule3))] Harry is furry.[(((triple13 triple15) -> rule1))] @2: Erin is furry.[(((triple4 ((triple6 triple3) -> rule3)) -> rule1))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
((triple10 ((triple12 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple7 triple8) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Erin is young.
("Erin" "is" "young" "+")
((triple6 triple3) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple12 triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple13 triple15) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4 ((triple6 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2