Bob is green. Bob is nice. Bob is round. Bob is young. Erin is quiet. Erin is red. Erin is young. If something is young and not quiet then it is nice. If something is green and not nice then it is not red. If something is green then it is not big. If something is round then it is green. If something is red and not young then it is round. Young things are round.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is young and not quiet then it is nice.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
If something is green and not nice then it is not red.
((("something" "is" "green" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "-"))
If something is green then it is not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is red and not young then it is round.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Bob is round.
True
1
proof
[(triple3 OR ((triple4) -> rule6))]
("Bob" "is" "round" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is not red.
False
1
inv-proof
[(triple6)]
("Erin" "is" "red" "-")
triple6
Erin is round.
True
2
proof
[(((triple7) -> rule6))]
("Erin" "is" "round" "+")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple7) -> rule6))]
("Erin" "is" "round" "-")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
True
3
proof
[(((((triple7) -> rule6)) -> rule4))]
("Erin" "is" "green" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not green.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule4))]
("Erin" "is" "green" "-")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not big.
True
4
proof
[(((((((triple7) -> rule6)) -> rule4)) -> rule3))]
("Erin" "is" "big" "-")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is big.
False
4
inv-proof
[(((((((triple7) -> rule6)) -> rule4)) -> rule3))]
("Erin" "is" "big" "+")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is green.[(triple1 OR ((triple3) -> rule4) OR ((((triple4) -> rule6)) -> rule4))] Bob is nice.[(triple2)] Bob is round.[(triple3 OR ((triple4) -> rule6))] Bob is young.[(triple4)] Erin is quiet.[(triple5)] Erin is red.[(triple6)] Erin is young.[(triple7)] @1: Bob is not big.[(((triple1) -> rule3) OR ((((triple3) -> rule4)) -> rule3) OR ((((((triple4) -> rule6)) -> rule4)) -> rule3))] Erin is round.[(((triple7) -> rule6))] @2: Erin is green.[(((((triple7) -> rule6)) -> rule4))] @3: Erin is not big.[(((((((triple7) -> rule6)) -> rule4)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
((triple3) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Bob is not big.
("Bob" "is" "big" "-")
((triple1) -> (rule3 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not big.
("Erin" "is" "big" "-")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3