Bob is young. Charlie is round. Erin is young. All nice, young things are round. All white, nice things are big. If Erin is young then Erin is blue. If something is young and not white then it is smart. If something is big and not white then it is young. If something is blue then it is not nice. If Charlie is young then Charlie is nice. If Erin is young and Erin is not nice then Erin is round.
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
All nice, young things are round.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All white, nice things are big.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Erin is young then Erin is blue.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "blue" "+"))
If something is young and not white then it is smart.
((("something" "is" "young" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "+"))
If something is big and not white then it is young.
((("something" "is" "big" "+") ("something" "is" "white" "~")) -> ("something" "is" "young" "+"))
If something is blue then it is not nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "-"))
If Charlie is young then Charlie is nice.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "nice" "+"))
If Erin is young and Erin is not nice then Erin is round.
((("Erin" "is" "young" "+") ("Erin" "is" "nice" "~")) -> ("Erin" "is" "round" "+"))
Charlie is round.
True
1
proof
[(triple2)]
("Charlie" "is" "round" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Erin is blue.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("Erin" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("Erin" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
True
5
proof
[(((triple3 ((((triple3) -> rule3)) -> rule6)) -> rule8))]
("Erin" "is" "round" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not round.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule3)) -> rule6)) -> rule8))]
("Erin" "is" "round" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is young.[(triple1)] Charlie is round.[(triple2)] Erin is young.[(triple3)] @1: Erin is blue.[(((triple3) -> rule3))] @2: Erin is not nice.[(((((triple3) -> rule3)) -> rule6))] @3: Erin is round.[(((triple3 ((((triple3) -> rule3)) -> rule6)) -> rule8))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3