Bob is blue. Bob is furry. Bob is kind. Bob is red. Bob is rough. Bob is smart. Erin is blue. Erin is kind. Erin is quiet. Harry is blue. Harry is quiet. Harry is red. Smart, red things are rough. Red things are smart. If something is quiet then it is smart.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Smart, red things are rough.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Harry is quiet.
True
1
proof
[(triple11)]
("Harry" "is" "quiet" "+")
triple11
Erin is not kind.
False
1
inv-proof
[(triple8)]
("Erin" "is" "kind" "-")
triple8
Harry is smart.
True
2
proof
[(((triple11) -> rule3) OR ((triple12) -> rule2))]
("Harry" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple12) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple9) -> rule3))]
("Erin" "is" "smart" "-")
((triple9) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is rough.
True
4
proof
[(((((triple11) -> rule3) triple12) -> rule1) OR ((((triple12) -> rule2) triple12) -> rule1))]
("Harry" "is" "rough" "+")
((((triple11) -> (rule3 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple12) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((((triple11) -> rule3) triple12) -> rule1) OR ((((triple12) -> rule2) triple12) -> rule1))]
("Harry" "is" "rough" "-")
((((triple11) -> (rule3 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple12) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is kind.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple6 triple4) -> rule1) OR ((((triple4) -> rule2) triple4) -> rule1))] Bob is smart.[(triple6 OR ((triple4) -> rule2))] Erin is blue.[(triple7)] Erin is kind.[(triple8)] Erin is quiet.[(triple9)] Harry is blue.[(triple10)] Harry is quiet.[(triple11)] Harry is red.[(triple12)] @1: Erin is smart.[(((triple9) -> rule3))] Harry is smart.[(((triple11) -> rule3) OR ((triple12) -> rule2))] @2: Harry is rough.[(((((triple11) -> rule3) triple12) -> rule1) OR ((((triple12) -> rule2) triple12) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple6 triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Erin is smart.
("Erin" "is" "smart" "+")
((triple9) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple11) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple12) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple11) -> (rule3 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple12) -> (rule2 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2