Bob is young. Charlie is round. Dave is nice. Erin is big. If someone is round and not big then they are quiet. If someone is green then they are quiet. If Bob is big then Bob is quiet. Young people are green. If someone is big and not round then they are nice. All big people are young.
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
If someone is round and not big then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "+"))
If someone is green then they are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is big then Bob is quiet.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "quiet" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is big and not round then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "nice" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Erin is big.
True
1
proof
[(triple4)]
("Erin" "is" "big" "+")
triple4
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Erin is young.
True
2
proof
[(((triple4) -> rule6))]
("Erin" "is" "young" "+")
((triple4) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "green" "-")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is green.
True
3
proof
[(((((triple4) -> rule6)) -> rule4))]
("Erin" "is" "green" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not green.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4))]
("Erin" "is" "green" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
True
4
proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule2))]
("Erin" "is" "quiet" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not quiet.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule2))]
("Erin" "is" "quiet" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is quiet.
Unknown
rconc
[@3: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Dave is quiet.
Unknown
rconc
[@3: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("Dave" "is" "quiet" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is young.[(triple1)] Charlie is round.[(triple2)] Dave is nice.[(triple3)] Erin is big.[(triple4)] @1: Bob is green.[(((triple1) -> rule4))] Erin is young.[(((triple4) -> rule6))] @2: Bob is quiet.[(((((triple1) -> rule4)) -> rule2))] Erin is green.[(((((triple4) -> rule6)) -> rule4))] @3: Erin is quiet.[(((((((triple4) -> rule6)) -> rule4)) -> rule2))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3