Dave is big. Fiona is nice. Gary is young. If someone is nice and white then they are red. If someone is young then they are red. If someone is nice then they are young. If someone is red and smart then they are young. White people are nice. Red, nice people are white. If someone is red then they are young. If someone is young then they are red.
Dave is big.
("Dave" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is nice and white then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is red and smart then they are young.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Red, nice people are white.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Gary is red.
True
2
proof
[(((triple3) -> rule2) OR ((triple3) -> rule8))]
("Gary" "is" "red" "+")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple3) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple3) -> rule8))]
("Gary" "is" "red" "-")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple3) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Fiona is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule3)) -> rule8))]
("Fiona" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule3)) -> rule8))]
("Fiona" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
True
5
proof
[(((((((triple2) -> rule3)) -> rule2) triple2) -> rule6) OR ((((((triple2) -> rule3)) -> rule8) triple2) -> rule6))]
("Fiona" "is" "white" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not white.
False
5
inv-proof
[(((((((triple2) -> rule3)) -> rule2) triple2) -> rule6) OR ((((((triple2) -> rule3)) -> rule8) triple2) -> rule6))]
("Fiona" "is" "white" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "white" "+")
Gary is not nice.
Unknown
inv-rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "-")
Dave is red.
Unknown
rconc
[@6: Dave is red.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule8 <- rule3 <- rule5 <- rule6 <- FAIL)]]
("Dave" "is" "red" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Dave is big.[(triple1)] Fiona is nice.[(triple2)] Gary is young.[(triple3)] @1: Fiona is young.[(((triple2) -> rule3))] Gary is red.[(((triple3) -> rule2) OR ((triple3) -> rule8))] @2: Fiona is red.[(((((triple2) -> rule3)) -> rule2) OR ((((triple2) -> rule3)) -> rule8))] @3: Fiona is white.[(((((((triple2) -> rule3)) -> rule2) triple2) -> rule6) OR ((((((triple2) -> rule3)) -> rule8) triple2) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
((triple2) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple3) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2)) triple2) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3