Dave is furry. Dave is rough. Dave is young. Erin is furry. Erin is young. Gary is white. Gary is young. All furry, white things are young. If something is smart then it is white. If something is young and green then it is white. If Erin is white then Erin is rough. If something is rough then it is nice. If something is young and furry then it is smart. If something is smart and rough then it is white. If something is rough and smart then it is white.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All furry, white things are young.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is young and green then it is white.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Erin is white then Erin is rough.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "rough" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is young and furry then it is smart.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is smart and rough then it is white.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is rough and smart then it is white.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Erin is young.
True
1
proof
[(triple5)]
("Erin" "is" "young" "+")
triple5
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Dave is smart.
True
3
proof
[(((triple3 triple1) -> rule6))]
("Dave" "is" "smart" "+")
((triple3 triple1) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
3
inv-proof
[(((triple3 triple1) -> rule6))]
("Dave" "is" "smart" "-")
((triple3 triple1) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
True
4
proof
[(((((triple3 triple1) -> rule6)) -> rule2) OR ((triple2 ((triple3 triple1) -> rule6)) -> rule8) OR ((((triple3 triple1) -> rule6) triple2) -> rule7))]
("Dave" "is" "white" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple2 ((triple3 triple1) -> (rule6 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 triple1) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not white.
False
4
inv-proof
[(((((triple3 triple1) -> rule6)) -> rule2) OR ((triple2 ((triple3 triple1) -> rule6)) -> rule8) OR ((((triple3 triple1) -> rule6) triple2) -> rule7))]
("Dave" "is" "white" "-")
((((triple3 triple1) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple2 ((triple3 triple1) -> (rule6 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 triple1) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is rough.
True
5
proof
[(((((((triple5 triple4) -> rule6)) -> rule2)) -> rule4))]
("Erin" "is" "rough" "+")
((((((triple5 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not rough.
False
5
inv-proof
[(((((((triple5 triple4) -> rule6)) -> rule2)) -> rule4))]
("Erin" "is" "rough" "-")
((((((triple5 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Dave is furry.[(triple1)] Dave is rough.[(triple2)] Dave is young.[(triple3)] Erin is furry.[(triple4)] Erin is young.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7)] @1: Dave is nice.[(((triple2) -> rule5))] Dave is smart.[(((triple3 triple1) -> rule6))] Erin is smart.[(((triple5 triple4) -> rule6))] @2: Dave is white.[(((((triple3 triple1) -> rule6)) -> rule2) OR ((triple2 ((triple3 triple1) -> rule6)) -> rule8) OR ((((triple3 triple1) -> rule6) triple2) -> rule7))] Erin is white.[(((((triple5 triple4) -> rule6)) -> rule2))] @3: Erin is rough.[(((((((triple5 triple4) -> rule6)) -> rule2)) -> rule4))] @4: Erin is nice.[(((((((((triple5 triple4) -> rule6)) -> rule2)) -> rule4)) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3 triple1) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5 triple4) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((triple2 ((triple3 triple1) -> (rule6 % int2))) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple3 triple1) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple5 triple4) -> (rule6 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple5 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((((((triple5 triple4) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4