Bob is big. Bob is blue. Bob is smart. Erin is smart. Fiona is furry. Harry is blue. Harry is furry. If Bob is young then Bob is smart. Blue, young people are smart. All quiet, smart people are green. If someone is furry then they are smart. If someone is smart then they are quiet. Blue, quiet people are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Bob is young then Bob is smart.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "smart" "+"))
Blue, young people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All quiet, smart people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is furry then they are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Blue, quiet people are big.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Erin is smart.
True
1
proof
[(triple4)]
("Erin" "is" "smart" "+")
triple4
Erin is not smart.
False
1
inv-proof
[(triple4)]
("Erin" "is" "smart" "-")
triple4
Harry is smart.
True
2
proof
[(((triple7) -> rule4))]
("Harry" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "quiet" "-")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple5) -> rule4)) -> rule5))]
("Fiona" "is" "quiet" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Erin is not green.
False
4
inv-proof
[(((((triple4) -> rule5) triple4) -> rule3))]
("Erin" "is" "green" "-")
((((triple4) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Harry is green.
True
6
proof
[(((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule3))]
("Harry" "is" "green" "+")
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) ((triple7) -> (rule4 % int3))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not big.
False
5
inv-proof
[(((triple6 ((((triple7) -> rule4)) -> rule5)) -> rule6))]
("Harry" "is" "big" "-")
((triple6 ((((triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "big" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "big" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is big.[(triple1 OR ((triple2 ((triple3) -> rule5)) -> rule6))] Bob is blue.[(triple2)] Bob is smart.[(triple3)] Erin is smart.[(triple4)] Fiona is furry.[(triple5)] Harry is blue.[(triple6)] Harry is furry.[(triple7)] @1: Bob is quiet.[(((triple3) -> rule5))] Erin is quiet.[(((triple4) -> rule5))] Fiona is smart.[(((triple5) -> rule4))] Harry is smart.[(((triple7) -> rule4))] @2: Bob is green.[(((((triple3) -> rule5) triple3) -> rule3))] Erin is green.[(((((triple4) -> rule5) triple4) -> rule3))] Fiona is quiet.[(((((triple5) -> rule4)) -> rule5))] Harry is quiet.[(((((triple7) -> rule4)) -> rule5))] @3: Fiona is green.[(((((((triple5) -> rule4)) -> rule5) ((triple5) -> rule4)) -> rule3))] Harry is big.[(((triple6 ((((triple7) -> rule4)) -> rule5)) -> rule6))] Harry is green.[(((((((triple7) -> rule4)) -> rule5) ((triple7) -> rule4)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple7) -> (rule4 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2)) ((triple5) -> (rule4 % int3))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple6 ((((triple7) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple7) -> (rule4 % int3))) -> (rule5 % int2)) ((triple7) -> (rule4 % int3))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3