Bob is not red. Charlie is red. Charlie is round. Dave is not white. Erin is nice. Erin is red. Erin is white. All nice people are white. Young people are not white. If Erin is not red then Erin is young. If Dave is not young then Dave is cold. If Charlie is red then Charlie is nice. If someone is round and white then they are not cold. If someone is white then they are smart. If Bob is white then Bob is not smart.
Bob is not red.
("Bob" "is" "red" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Young people are not white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "-"))
If Erin is not red then Erin is young.
((("Erin" "is" "red" "~")) -> ("Erin" "is" "young" "+"))
If Dave is not young then Dave is cold.
((("Dave" "is" "young" "~")) -> ("Dave" "is" "cold" "+"))
If Charlie is red then Charlie is nice.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "nice" "+"))
If someone is round and white then they are not cold.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "-"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Bob is white then Bob is not smart.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "-"))
Bob is not red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Erin is not white.
False
1
inv-proof
[(triple7 OR ((triple5) -> rule1))]
("Erin" "is" "white" "-")
triple7
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is nice.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Charlie" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not cold.
True
5
proof
[(((triple3 ((((triple2) -> rule5)) -> rule1)) -> rule6))]
("Charlie" "is" "cold" "-")
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is cold.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule5)) -> rule1)) -> rule6))]
("Charlie" "is" "cold" "+")
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "smart" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is not red.[(triple1)] Charlie is red.[(triple2)] Charlie is round.[(triple3)] Dave is not white.[(triple4)] Erin is nice.[(triple5)] Erin is red.[(triple6)] Erin is white.[(triple7 OR ((triple5) -> rule1))] @1: Charlie is nice.[(((triple2) -> rule5))] Erin is smart.[(((triple7) -> rule7) OR ((((triple5) -> rule1)) -> rule7))] @2: Charlie is white.[(((((triple2) -> rule5)) -> rule1))] @3: Charlie is not cold.[(((triple3 ((((triple2) -> rule5)) -> rule1)) -> rule6))] Charlie is smart.[(((((((triple2) -> rule5)) -> rule1)) -> rule7))]
Bob is not red.
("Bob" "is" "red" "-")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Dave is not white.
("Dave" "is" "white" "-")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple5) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3