Bob is blue. Bob is not quiet. Bob is white. Dave is quiet. Dave is smart. Dave is white. Erin is not blue. Erin is quiet. Erin is white. Harry is green. All green people are red. All quiet, green people are blue. If Bob is quiet then Bob is not red. Green people are quiet. Blue people are not smart. If Harry is white then Harry is not big. If someone is quiet and not smart then they are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All quiet, green people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Bob is quiet then Bob is not red.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "-"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are not smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "-"))
If Harry is white then Harry is not big.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "big" "-"))
If someone is quiet and not smart then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "white" "+"))
Dave is smart.
True
1
proof
[(triple5)]
("Dave" "is" "smart" "+")
triple5
Harry is not green.
False
1
inv-proof
[(triple10)]
("Harry" "is" "green" "-")
triple10
Harry is quiet.
True
2
proof
[(((triple10) -> rule4))]
("Harry" "is" "quiet" "+")
((triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple10) -> rule1))]
("Harry" "is" "red" "-")
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
True
4
proof
[(((((triple10) -> rule4) triple10) -> rule2))]
("Harry" "is" "blue" "+")
((((triple10) -> (rule4 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple10) -> rule4) triple10) -> rule2))]
("Harry" "is" "blue" "-")
((((triple10) -> (rule4 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not smart.
True
5
proof
[(((((((triple10) -> rule4) triple10) -> rule2)) -> rule5))]
("Harry" "is" "smart" "-")
((((((triple10) -> (rule4 % int3)) triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
False
5
inv-proof
[(((((((triple10) -> rule4) triple10) -> rule2)) -> rule5))]
("Harry" "is" "smart" "+")
((((((triple10) -> (rule4 % int3)) triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is white.
True
8
proof
[(((((triple10) -> rule4) ((((((triple10) -> rule4) triple10) -> rule2)) -> rule5)) -> rule7))]
("Harry" "is" "white" "+")
((((triple10) -> (rule4 % int4)) ((((((triple10) -> (rule4 % int4)) triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not white.
False
8
inv-proof
[(((((triple10) -> rule4) ((((((triple10) -> rule4) triple10) -> rule2)) -> rule5)) -> rule7))]
("Harry" "is" "white" "-")
((((triple10) -> (rule4 % int4)) ((((((triple10) -> (rule4 % int4)) triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not big.
True
9
proof
[(((((((triple10) -> rule4) ((((((triple10) -> rule4) triple10) -> rule2)) -> rule5)) -> rule7)) -> rule6))]
("Harry" "is" "big" "-")
((((((triple10) -> (rule4 % int5)) ((((((triple10) -> (rule4 % int5)) triple10) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Harry is big.
False
9
inv-proof
[(((((((triple10) -> rule4) ((((((triple10) -> rule4) triple10) -> rule2)) -> rule5)) -> rule7)) -> rule6))]
("Harry" "is" "big" "+")
((((((triple10) -> (rule4 % int5)) ((((((triple10) -> (rule4 % int5)) triple10) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Dave is red.
Unknown
rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "blue" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is not quiet.[(triple2)] Bob is white.[(triple3)] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Dave is white.[(triple6)] Erin is not blue.[(triple7)] Erin is quiet.[(triple8)] Erin is white.[(triple9)] Harry is green.[(triple10)] @1: Bob is not smart.[(((triple1) -> rule5))] Harry is quiet.[(((triple10) -> rule4))] Harry is red.[(((triple10) -> rule1))] @2: Harry is blue.[(((((triple10) -> rule4) triple10) -> rule2))] @3: Harry is not smart.[(((((((triple10) -> rule4) triple10) -> rule2)) -> rule5))] @4: Harry is white.[(((((triple10) -> rule4) ((((((triple10) -> rule4) triple10) -> rule2)) -> rule5)) -> rule7))] @5: Harry is not big.[(((((((triple10) -> rule4) ((((((triple10) -> rule4) triple10) -> rule2)) -> rule5)) -> rule7)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is not blue.
("Erin" "is" "blue" "-")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Bob is not smart.
("Bob" "is" "smart" "-")
((triple1) -> (rule5 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple10) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple10) -> (rule4 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
((((((triple10) -> (rule4 % int3)) triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((triple10) -> (rule4 % int4)) ((((((triple10) -> (rule4 % int4)) triple10) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not big.
("Harry" "is" "big" "-")
((((((triple10) -> (rule4 % int5)) ((((((triple10) -> (rule4 % int5)) triple10) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
int5