Dave is smart. Erin is big. Erin is green. If Erin is young then Erin is smart. If Dave is smart then Dave is green. All green, blue things are big. Rough, smart things are red. Green things are rough. All green, big things are young.
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
If Erin is young then Erin is smart.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "smart" "+"))
If Dave is smart then Dave is green.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
All green, blue things are big.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Rough, smart things are red.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All green, big things are young.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Erin is not green.
False
1
inv-proof
[(triple3)]
("Erin" "is" "green" "-")
triple3
Dave is green.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "green" "+")
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is not young.
False
3
inv-proof
[(((triple3 triple2) -> rule6))]
("Erin" "is" "young" "-")
((triple3 triple2) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is smart.
True
4
proof
[(((((triple3 triple2) -> rule6)) -> rule1))]
("Erin" "is" "smart" "+")
((((triple3 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not smart.
False
4
inv-proof
[(((((triple3 triple2) -> rule6)) -> rule1))]
("Erin" "is" "smart" "-")
((((triple3 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
True
7
proof
[(((((triple3) -> rule5) ((((triple3 triple2) -> rule6)) -> rule1)) -> rule4))]
("Erin" "is" "red" "+")
((((triple3) -> (rule5 % int4)) ((((triple3 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is not red.
False
7
inv-proof
[(((((triple3) -> rule5) ((((triple3 triple2) -> rule6)) -> rule1)) -> rule4))]
("Erin" "is" "red" "-")
((((triple3) -> (rule5 % int4)) ((((triple3 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is young.
Unknown
rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "young" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Dave is smart.[(triple1)] Erin is big.[(triple2)] Erin is green.[(triple3)] @1: Dave is green.[(((triple1) -> rule2))] Erin is rough.[(((triple3) -> rule5))] Erin is young.[(((triple3 triple2) -> rule6))] @2: Dave is rough.[(((((triple1) -> rule2)) -> rule5))] Erin is smart.[(((((triple3 triple2) -> rule6)) -> rule1))] @3: Dave is red.[(((((((triple1) -> rule2)) -> rule5) triple1) -> rule4))] Erin is red.[(((((triple3) -> rule5) ((((triple3 triple2) -> rule6)) -> rule1)) -> rule4))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple3 triple2) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple3 triple2) -> (rule6 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule5 % int4)) ((((triple3 triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4