Anne is green. Bob is nice. Bob is quiet. Bob is smart. Erin is big. Harry is not quiet. Harry is young. If something is rough then it is nice. All big things are rough. If something is quiet and big then it is not rough. Smart things are green. If something is young and nice then it is green. If Erin is rough and Erin is nice then Erin is smart. All green things are young. If Bob is rough and Bob is quiet then Bob is nice.
Anne is green.
("Anne" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is young.
("Harry" "is" "young" "+")
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and big then it is not rough.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is young and nice then it is green.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Erin is rough and Erin is nice then Erin is smart.
((("Erin" "is" "rough" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "smart" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Bob is rough and Bob is quiet then Bob is nice.
((("Bob" "is" "rough" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "nice" "+"))
Bob is smart.
True
1
proof
[(triple4)]
("Bob" "is" "smart" "+")
triple4
Harry is quiet.
False
1
inv-proof
[(triple6)]
("Harry" "is" "quiet" "+")
triple6
Bob is green.
True
2
proof
[(((triple4) -> rule4))]
("Bob" "is" "green" "+")
((triple4) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple4) -> rule4))]
("Bob" "is" "green" "-")
((triple4) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is nice.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("Erin" "is" "nice" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule7))]
("Bob" "is" "young" "-")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is smart.
True
6
proof
[(((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6))]
("Erin" "is" "smart" "+")
((((triple5) -> (rule2 % int3)) ((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6))]
("Erin" "is" "smart" "-")
((((triple5) -> (rule2 % int3)) ((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
True
7
proof
[(((((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6)) -> rule4))]
("Erin" "is" "green" "+")
((((((triple5) -> (rule2 % int4)) ((((triple5) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is not green.
False
7
inv-proof
[(((((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6)) -> rule4))]
("Erin" "is" "green" "-")
((((((triple5) -> (rule2 % int4)) ((((triple5) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
True
8
proof
[(((((((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
("Erin" "is" "young" "+")
((((((((triple5) -> (rule2 % int5)) ((((triple5) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Erin is not young.
False
8
inv-proof
[(((((((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
("Erin" "is" "young" "-")
((((((((triple5) -> (rule2 % int5)) ((((triple5) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is green.
Unknown
rconc
[@3: Harry is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("Harry" "is" "green" "+")
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "nice" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "nice" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Bob is smart.[(triple4)] Erin is big.[(triple5)] Harry is not quiet.[(triple6)] Harry is young.[(triple7)] @1: Anne is young.[(((triple1) -> rule7))] Bob is green.[(((triple4) -> rule4))] Erin is rough.[(((triple5) -> rule2))] @2: Bob is young.[(((((triple4) -> rule4)) -> rule7))] Erin is nice.[(((((triple5) -> rule2)) -> rule1))] @3: Erin is smart.[(((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6))] @4: Erin is green.[(((((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6)) -> rule4))] @5: Erin is young.[(((((((((triple5) -> rule2) ((((triple5) -> rule2)) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple4) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple5) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple5) -> (rule2 % int3)) ((((triple5) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple5) -> (rule2 % int4)) ((((triple5) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((((((triple5) -> (rule2 % int5)) ((((triple5) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5