Bob is young. Charlie is blue. Charlie is not smart. Erin is blue. Erin is green. Harry is blue. Harry is cold. If someone is cold and quiet then they are smart. If someone is blue and young then they are cold. If Erin is green then Erin is quiet. All quiet, blue people are young. If Harry is young then Harry is green. All young, smart people are quiet. Smart people are white.
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is cold and quiet then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and young then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If Erin is green then Erin is quiet.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "quiet" "+"))
All quiet, blue people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If Harry is young then Harry is green.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "green" "+"))
All young, smart people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is smart.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "smart" "+")
triple3
Erin is quiet.
True
2
proof
[(((triple5) -> rule3))]
("Erin" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple5) -> rule3))]
("Erin" "is" "quiet" "-")
((triple5) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
True
4
proof
[(((((triple5) -> rule3) triple4) -> rule4))]
("Erin" "is" "young" "+")
((((triple5) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not young.
False
4
inv-proof
[(((((triple5) -> rule3) triple4) -> rule4))]
("Erin" "is" "young" "-")
((((triple5) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
True
6
proof
[(((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2))]
("Erin" "is" "cold" "+")
((triple4 ((((triple5) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is not cold.
False
6
inv-proof
[(((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2))]
("Erin" "is" "cold" "-")
((triple4 ((((triple5) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is smart.
True
9
proof
[(((((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2) ((triple5) -> rule3)) -> rule1))]
("Erin" "is" "smart" "+")
((((triple4 ((((triple5) -> (rule3 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2)) ((triple5) -> (rule3 % int4))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is not smart.
False
9
inv-proof
[(((((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2) ((triple5) -> rule3)) -> rule1))]
("Erin" "is" "smart" "-")
((((triple4 ((((triple5) -> (rule3 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2)) ((triple5) -> (rule3 % int4))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is white.
True
10
proof
[(((((((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2) ((triple5) -> rule3)) -> rule1)) -> rule7))]
("Erin" "is" "white" "+")
((((((triple4 ((((triple5) -> (rule3 % int5)) triple4) -> (rule4 % int4))) -> (rule2 % int3)) ((triple5) -> (rule3 % int5))) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Erin is not white.
False
10
inv-proof
[(((((((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2) ((triple5) -> rule3)) -> rule1)) -> rule7))]
("Erin" "is" "white" "-")
((((((triple4 ((((triple5) -> (rule3 % int5)) triple4) -> (rule4 % int4))) -> (rule2 % int3)) ((triple5) -> (rule3 % int5))) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is white.
Unknown
rconc
[@3: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule2 <- FAIL)]]
("Bob" "is" "white" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Harry" "is" "smart" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is young.[(triple1)] Charlie is blue.[(triple2)] Charlie is not smart.[(triple3)] Erin is blue.[(triple4)] Erin is green.[(triple5)] Harry is blue.[(triple6)] Harry is cold.[(triple7)] @1: Erin is quiet.[(((triple5) -> rule3))] @2: Erin is young.[(((((triple5) -> rule3) triple4) -> rule4))] @3: Erin is cold.[(((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2))] @4: Erin is smart.[(((((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2) ((triple5) -> rule3)) -> rule1))] @5: Erin is white.[(((((((triple4 ((((triple5) -> rule3) triple4) -> rule4)) -> rule2) ((triple5) -> rule3)) -> rule1)) -> rule7))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((((triple5) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple4 ((((triple5) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((triple4 ((((triple5) -> (rule3 % int4)) triple4) -> (rule4 % int3))) -> (rule2 % int2)) ((triple5) -> (rule3 % int4))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((((((triple4 ((((triple5) -> (rule3 % int5)) triple4) -> (rule4 % int4))) -> (rule2 % int3)) ((triple5) -> (rule3 % int5))) -> (rule1 % int2))) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5