Charlie is round. Fiona is blue. Fiona is quiet. Fiona is young. Gary is blue. Gary is not young. Harry is quiet. Harry is rough. Harry is round. Harry is smart. If Harry is smart and Harry is big then Harry is round. All round things are smart. If something is smart then it is big.
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is smart and Harry is big then Harry is round.
((("Harry" "is" "smart" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "round" "+"))
All round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Harry is rough.
True
1
proof
[(triple8)]
("Harry" "is" "rough" "+")
triple8
Harry is not quiet.
False
1
inv-proof
[(triple7)]
("Harry" "is" "quiet" "-")
triple7
Harry is big.
True
2
proof
[(((triple10) -> rule3) OR ((((triple9) -> rule2)) -> rule3))]
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Charlie is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "big" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Charlie is round.[(triple1)] Fiona is blue.[(triple2)] Fiona is quiet.[(triple3)] Fiona is young.[(triple4)] Gary is blue.[(triple5)] Gary is not young.[(triple6)] Harry is quiet.[(triple7)] Harry is rough.[(triple8)] Harry is round.[(triple9 OR ((triple10 ((triple10) -> rule3)) -> rule1))] Harry is smart.[(triple10 OR ((triple9) -> rule2))] @1: Charlie is smart.[(((triple1) -> rule2))] Harry is big.[(((triple10) -> rule3) OR ((((triple9) -> rule2)) -> rule3))] @2: Charlie is big.[(((((triple1) -> rule2)) -> rule3))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is not young.
("Gary" "is" "young" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple10 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2