Bob is blue. Bob is kind. Bob is smart. Bob is young. Erin is blue. Fiona is red. Fiona is not smart. Harry is blue. Harry is not kind. Harry is nice. If Erin is smart and Erin is blue then Erin is furry. Kind, blue things are smart. Blue things are smart. All blue things are smart. If something is furry and not kind then it is not red. If something is blue and young then it is not red. Furry things are young. If Erin is not red then Erin is nice. If Bob is not young and Bob is not red then Bob is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
If Erin is smart and Erin is blue then Erin is furry.
((("Erin" "is" "smart" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "furry" "+"))
Kind, blue things are smart.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is furry and not kind then it is not red.
((("something" "is" "furry" "+") ("something" "is" "kind" "~")) -> ("something" "is" "red" "-"))
If something is blue and young then it is not red.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If Erin is not red then Erin is nice.
((("Erin" "is" "red" "~")) -> ("Erin" "is" "nice" "+"))
If Bob is not young and Bob is not red then Bob is nice.
((("Bob" "is" "young" "~") ("Bob" "is" "red" "~")) -> ("Bob" "is" "nice" "+"))
Bob is smart.
True
1
proof
[(triple3 OR ((triple1) -> rule3) OR ((triple1) -> rule4) OR ((triple2 triple1) -> rule2))]
("Bob" "is" "smart" "+")
triple3
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2 triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Bob is not red.
True
3
proof
[(((triple1 triple4) -> rule6))]
("Bob" "is" "red" "-")
((triple1 triple4) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Harry is not smart.
False
2
inv-proof
[(((triple8) -> rule3) OR ((triple8) -> rule4))]
("Harry" "is" "smart" "-")
((triple8) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple8) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is furry.
True
4
proof
[(((((triple5) -> rule3) triple5) -> rule1) OR ((((triple5) -> rule4) triple5) -> rule1))]
("Erin" "is" "furry" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not furry.
False
4
inv-proof
[(((((triple5) -> rule3) triple5) -> rule1) OR ((((triple5) -> rule4) triple5) -> rule1))]
("Erin" "is" "furry" "-")
((((triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
True
5
proof
[(((((((triple5) -> rule3) triple5) -> rule1)) -> rule7) OR ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7))]
("Erin" "is" "young" "+")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not young.
False
5
inv-proof
[(((((((triple5) -> rule3) triple5) -> rule1)) -> rule7) OR ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7))]
("Erin" "is" "young" "-")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not red.
True
7
proof
[(((triple5 ((((((triple5) -> rule3) triple5) -> rule1)) -> rule7)) -> rule6) OR ((triple5 ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7)) -> rule6))]
("Erin" "is" "red" "-")
((triple5 ((((((triple5) -> (rule3 % int4)) triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((triple5 ((((((triple5) -> (rule4 % int4)) triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is red.
False
7
inv-proof
[(((triple5 ((((((triple5) -> rule3) triple5) -> rule1)) -> rule7)) -> rule6) OR ((triple5 ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7)) -> rule6))]
("Erin" "is" "red" "+")
((triple5 ((((((triple5) -> (rule3 % int4)) triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((triple5 ((((((triple5) -> (rule4 % int4)) triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is nice.
True
8
proof
[(((((triple5 ((((((triple5) -> rule3) triple5) -> rule1)) -> rule7)) -> rule6)) -> rule8) OR ((((triple5 ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7)) -> rule6)) -> rule8))]
("Erin" "is" "nice" "+")
((((triple5 ((((((triple5) -> (rule3 % int5)) triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
((((triple5 ((((((triple5) -> (rule4 % int5)) triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Erin is not nice.
False
8
inv-proof
[(((((triple5 ((((((triple5) -> rule3) triple5) -> rule1)) -> rule7)) -> rule6)) -> rule8) OR ((((triple5 ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7)) -> rule6)) -> rule8))]
("Erin" "is" "nice" "-")
((((triple5 ((((((triple5) -> (rule3 % int5)) triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
((((triple5 ((((((triple5) -> (rule4 % int5)) triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "young" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Bob" "is" "nice" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2)] Bob is smart.[(triple3 OR ((triple1) -> rule3) OR ((triple1) -> rule4) OR ((triple2 triple1) -> rule2))] Bob is young.[(triple4)] Erin is blue.[(triple5)] Fiona is not smart.[(triple7)] Fiona is red.[(triple6)] Harry is blue.[(triple8)] Harry is nice.[(triple10)] Harry is not kind.[(triple9)] @1: Bob is not red.[(((triple1 triple4) -> rule6))] Erin is smart.[(((triple5) -> rule3) OR ((triple5) -> rule4))] Harry is smart.[(((triple8) -> rule3) OR ((triple8) -> rule4))] @2: Erin is furry.[(((((triple5) -> rule3) triple5) -> rule1) OR ((((triple5) -> rule4) triple5) -> rule1))] @3: Erin is young.[(((((((triple5) -> rule3) triple5) -> rule1)) -> rule7) OR ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7))] @4: Erin is not red.[(((triple5 ((((((triple5) -> rule3) triple5) -> rule1)) -> rule7)) -> rule6) OR ((triple5 ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7)) -> rule6))] @5: Erin is nice.[(((((triple5 ((((((triple5) -> rule3) triple5) -> rule1)) -> rule7)) -> rule6)) -> rule8) OR ((((triple5 ((((((triple5) -> rule4) triple5) -> rule1)) -> rule7)) -> rule6)) -> rule8))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2 triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Bob is not red.
("Bob" "is" "red" "-")
((triple1 triple4) -> (rule6 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple5) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple8) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple5) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((((triple5) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not red.
("Erin" "is" "red" "-")
((triple5 ((((((triple5) -> (rule3 % int4)) triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
((triple5 ((((((triple5) -> (rule4 % int4)) triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
((((triple5 ((((((triple5) -> (rule3 % int5)) triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
((((triple5 ((((((triple5) -> (rule4 % int5)) triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5