Dave is smart. Erin is smart. Gary is quiet. Harry is rough. All quiet people are young. If Gary is rough then Gary is quiet. If Dave is young and Dave is quiet then Dave is rough. Smart, young people are furry. Furry people are blue. Quiet people are smart.
Dave is smart.
("Dave" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Gary is rough then Gary is quiet.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "quiet" "+"))
If Dave is young and Dave is quiet then Dave is rough.
((("Dave" "is" "young" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "rough" "+"))
Smart, young people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Gary is young.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "young" "+")
((triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "smart" "-")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
True
5
proof
[(((((triple3) -> rule6) ((triple3) -> rule1)) -> rule4))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not furry.
False
5
inv-proof
[(((((triple3) -> rule6) ((triple3) -> rule1)) -> rule4))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule6 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is blue.
True
6
proof
[(((((((triple3) -> rule6) ((triple3) -> rule1)) -> rule4)) -> rule5))]
("Gary" "is" "blue" "+")
((((((triple3) -> (rule6 % int4)) ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not blue.
False
6
inv-proof
[(((((((triple3) -> rule6) ((triple3) -> rule1)) -> rule4)) -> rule5))]
("Gary" "is" "blue" "-")
((((((triple3) -> (rule6 % int4)) ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Dave is smart.[(triple1)] Erin is smart.[(triple2)] Gary is quiet.[(triple3)] Harry is rough.[(triple4)] @1: Gary is smart.[(((triple3) -> rule6))] Gary is young.[(((triple3) -> rule1))] @2: Gary is furry.[(((((triple3) -> rule6) ((triple3) -> rule1)) -> rule4))] @3: Gary is blue.[(((((((triple3) -> rule6) ((triple3) -> rule1)) -> rule4)) -> rule5))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple3) -> (rule6 % int4)) ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4