Dave is big. Dave is cold. Dave is rough. Erin is big. Fiona is big. Gary is cold. Gary is rough. If someone is nice then they are big. All big people are green. Blue people are big. All green people are round. Nice people are rough. Big, green people are blue. Nice, big people are blue. Rough people are blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Big, green people are blue.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Nice, big people are blue.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple1 OR ((((triple3) -> rule8)) -> rule3))]
("Dave" "is" "big" "+")
triple1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Erin is not big.
False
1
inv-proof
[(triple4)]
("Erin" "is" "big" "-")
triple4
Dave is blue.
True
2
proof
[(((triple3) -> rule8) OR ((triple1 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "blue" "+")
((triple3) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is not green.
False
2
inv-proof
[(((triple4) -> rule2))]
("Erin" "is" "green" "-")
((triple4) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is big.
True
3
proof
[(((((triple7) -> rule8)) -> rule3))]
("Gary" "is" "big" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule4))]
("Erin" "is" "round" "-")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is green.
True
4
proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule2))]
("Gary" "is" "green" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not green.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule2))]
("Gary" "is" "green" "-")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "rough" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Dave is big.[(triple1 OR ((((triple3) -> rule8)) -> rule3))] Dave is cold.[(triple2)] Dave is rough.[(triple3)] Erin is big.[(triple4)] Fiona is big.[(triple5)] Gary is cold.[(triple6)] Gary is rough.[(triple7)] @1: Dave is blue.[(((triple3) -> rule8) OR ((triple1 ((triple1) -> rule2)) -> rule6))] Dave is green.[(((triple1) -> rule2) OR ((((((triple3) -> rule8)) -> rule3)) -> rule2))] Erin is green.[(((triple4) -> rule2))] Fiona is green.[(((triple5) -> rule2))] Gary is blue.[(((triple7) -> rule8))] @2: Dave is round.[(((((triple1) -> rule2)) -> rule4) OR ((((((((triple3) -> rule8)) -> rule3)) -> rule2)) -> rule4))] Erin is blue.[(((triple4 ((triple4) -> rule2)) -> rule6))] Erin is round.[(((((triple4) -> rule2)) -> rule4))] Fiona is blue.[(((triple5 ((triple5) -> rule2)) -> rule6))] Fiona is round.[(((((triple5) -> rule2)) -> rule4))] Gary is big.[(((((triple7) -> rule8)) -> rule3))] @3: Gary is green.[(((((((triple7) -> rule8)) -> rule3)) -> rule2))] @4: Gary is round.[(((((((((triple7) -> rule8)) -> rule3)) -> rule2)) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((((triple3) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5 ((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4