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