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